--- a/src/Pure/General/pretty.ML Sat Oct 26 20:18:51 2024 +0200
+++ b/src/Pure/General/pretty.ML Sun Oct 27 11:02:21 2024 +0100
@@ -315,8 +315,8 @@
val body' = map out body;
in
Block
- {markup = #markup ops (ML_Pretty.context_markup context),
- open_block = ML_Pretty.context_open_block context,
+ {markup = #markup ops (ML_Pretty.markup_get context),
+ open_block = ML_Pretty.open_block_detect context,
consistent = consistent,
indent = indent,
body = body',
--- a/src/Pure/ML/ml_pretty.ML Sat Oct 26 20:18:51 2024 +0200
+++ b/src/Pure/ML/ml_pretty.ML Sun Oct 27 11:02:21 2024 +0100
@@ -7,9 +7,9 @@
signature ML_PRETTY =
sig
datatype context = datatype PolyML.context
- val context_markup: PolyML.context list -> string * string
+ val markup_get: PolyML.context list -> string * string
val markup_context: string * string -> PolyML.context list
- val context_open_block: PolyML.context list -> bool
+ val open_block_detect: PolyML.context list -> bool
val open_block_context: bool -> PolyML.context list
datatype pretty = datatype PolyML.pretty
val block: pretty list -> pretty
@@ -37,7 +37,7 @@
datatype context = datatype PolyML.context;
-fun context_property context name =
+fun get_property context name =
(case List.find (fn ContextProperty (a, _) => name = a | _ => false) context of
SOME (ContextProperty (_, b)) => b
| _ => "");
@@ -48,10 +48,10 @@
val markup_bg = "markup_bg";
val markup_en = "markup_en";
-fun context_markup context =
+fun markup_get context =
let
- val bg = context_property context markup_bg;
- val en = context_property context markup_en;
+ val bg = get_property context markup_bg;
+ val en = get_property context markup_en;
in (bg, en) end;
fun markup_context (bg, en) =
@@ -63,7 +63,7 @@
val open_block = ContextProperty ("open_block", "true");
-val context_open_block = List.exists (fn c => c = open_block);
+val open_block_detect = List.exists (fn c => c = open_block);
fun open_block_context false = []
| open_block_context true = [open_block];