# HG changeset patch
# User wenzelm
# Date 1730023341 -3600
# Node ID 8300511f4c45cfbccd8eac84870906fcf4951b7b
# Parent  2daa7b2ef46e7429654446bb967e461b4e35467a
clarified signature;

diff -r 2daa7b2ef46e -r 8300511f4c45 src/Pure/General/pretty.ML
--- 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',
diff -r 2daa7b2ef46e -r 8300511f4c45 src/Pure/ML/ml_pretty.ML
--- 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];