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;