# HG changeset patch
# User wenzelm
# Date 1726077909 -7200
# Node ID a392351d1ed432d5f2230cc466f26f7c4b13c495
# Parent  aff85c86737b09ac2e276d43560c47d9305fe27f
more robust: global ML name space for markup elements;

diff -r aff85c86737b -r a392351d1ed4 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Sep 11 19:59:10 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Sep 11 20:05:09 2024 +0200
@@ -276,6 +276,8 @@
   val simp_trace_hintN: string
   val simp_trace_ignoreN: string
   val simp_trace_cancel: serial -> Properties.T
+  val code_presentationN: string
+  val stmt_nameN: string
   type output = Output.output * Output.output
   type ops = {output: T -> output}
   val no_output: output
@@ -838,6 +840,12 @@
 fun simp_trace_cancel i = [function "simp_trace_cancel", (serialN, Value.print_int i)];
 
 
+(* code generator *)
+
+val code_presentationN = "code_presentation";
+val stmt_nameN = "stmt_name";
+
+
 
 (** print mode operations **)
 
diff -r aff85c86737b -r a392351d1ed4 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Wed Sep 11 19:59:10 2024 +0200
+++ b/src/Tools/Code/code_printer.ML	Wed Sep 11 20:05:09 2024 +0200
@@ -113,9 +113,6 @@
       error (s ^ ",\nin equation " ^ Thm.string_of_thm_global thy thm)
   | eqn_error _ NONE s = error s;
 
-val code_presentationN = "code_presentation";
-val stmt_nameN = "stmt_name";
-
 
 (** assembling and printing text pieces **)
 
@@ -136,7 +133,7 @@
 val indent = Pretty.indent;
 
 fun markup_stmt sym =
-  Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]);
+  Pretty.mark (Markup.code_presentationN, [(Markup.stmt_nameN, Code_Symbol.marker sym)]);
 
 fun filter_presentation [] xml =
       Bytes.build (XML.traverse_texts Bytes.add xml)
@@ -144,8 +141,8 @@
       let
         val presentation_idents = map Code_Symbol.marker presentation_syms
         fun is_selected (name, attrs) =
-          name = code_presentationN
-          andalso member (op =) presentation_idents (the (Properties.get attrs stmt_nameN));
+          name = Markup.code_presentationN
+          andalso member (op =) presentation_idents (the (Properties.get attrs Markup.stmt_nameN));
         fun add_content_with_space tree (is_first, buf) =
           buf
           |> not is_first ? Bytes.add "\n\n"