diff --git a/pinc/DifferenceEngineWrapperTable.inc b/pinc/DifferenceEngineWrapperTable.inc index 06369af57..60470900b 100644 --- a/pinc/DifferenceEngineWrapperTable.inc +++ b/pinc/DifferenceEngineWrapperTable.inc @@ -59,7 +59,7 @@ class DifferenceEngineWrapperTable extends DifferenceEngineWrapper /** * Override default css for DP customizations */ -function get_DifferenceEngine_css_data() +function get_DifferenceEngine_css_data($font_family) { return " .diff-otitle, @@ -70,7 +70,7 @@ function get_DifferenceEngine_css_data() .diff-addedline, .diff-deletedline, .diff-context { - font-family: DP Sans Mono; + font-family: $font_family, monospace; } /* Adjust padding to prevent descenders from being chopped off. Task 1936 */ .diff-deletedline .diffchange, diff --git a/tools/project_manager/diff.php b/tools/project_manager/diff.php index 2c03fb6fa..4f29cda6d 100644 --- a/tools/project_manager/diff.php +++ b/tools/project_manager/diff.php @@ -26,6 +26,12 @@ $only_nonempty_diffs = @$_GET['only_nonempty_diffs'] === 'on'; $bb_diffs = (@$_GET['bb_diffs'] === 'on' and user_can_mentor_in_any_round()); +$user_diff_font = Settings::get_Settings(User::current_username())->get_value("diff_font", "DP Sans Mono"); +$diff_fonts = array_diff(array_values(get_available_proofreading_font_faces()), ['']); +$diff_font = get_enumerated_param($_GET, "diff_font", $user_diff_font, $diff_fonts); +if ($diff_font != $user_diff_font) { + Settings::get_Settings(User::current_username())->set_value("diff_font", $diff_font); +} $project = new Project($projectid); $state = $project->state; @@ -92,7 +98,7 @@ $image_url = "$code_url/tools/page_browser.php?project=$projectid&imagefile=$image"; $image_link = sprintf($link_text, new_window_link($image_url, $image)); $extra_args = [ - "css_data" => get_DifferenceEngine_css_data(), + "css_data" => get_DifferenceEngine_css_data($diff_font), "js_data" => " function copyToClip(textstring) { navigator.clipboard.writeText(textstring).catch(function () {alert('Unable to copy!');}); @@ -113,7 +119,8 @@ function copyToClip(textstring) { $L_user, $format, $only_nonempty_diffs, - $bb_diffs + $bb_diffs, + $diff_font ); echo $navigation_text; @@ -183,8 +190,11 @@ function get_navigation( $L_user, $format, $only_nonempty_diffs, - $bb_diffs + $bb_diffs, + $diff_font ) { + global $diff_fonts; + $navigation_text = ""; $jump_to_js = "this.form.image.value=this.form.jumpto[this.form.jumpto.selectedIndex].value; this.form.submit();"; @@ -273,6 +283,17 @@ function get_navigation( $navigation_text .= "\n\n"; $navigation_text .= "\n\n"; + + $navigation_text .= " · "; + + $navigation_text .= "\n\n"; + $navigation_text .= "\n"; + $navigation_text .= "\n\n"; return $navigation_text;