# HG changeset patch
# User wenzelm
# Date 1725623383 -7200
# Node ID 0f820da558f99e08bc59a651c0216069f61c9cb1
# Parent  7d8b1ed1f74844766d951584100a138205c64e46
clarified signature and modules;

diff -r 7d8b1ed1f748 -r 0f820da558f9 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Fri Sep 06 13:19:18 2024 +0200
+++ b/src/Pure/General/pretty.ML	Fri Sep 06 13:49:43 2024 +0200
@@ -437,12 +437,6 @@
 
 end;
 
-
-(** toplevel pretty printing **)
-
-val _ = ML_system_pp (fn d => fn _ => ML_Pretty.prune (d + 1) o to_ML o quote);
-val _ = ML_system_pp (fn _ => fn _ => to_ML o position);
-
 end;
 
 structure ML_Pretty: ML_PRETTY =
@@ -450,3 +444,22 @@
   open ML_Pretty;
   val string_of = Pretty.string_of o Pretty.from_ML;
 end;
+
+
+
+(** toplevel pretty printing **)
+
+val _ = ML_system_pp (fn d => fn _ => ML_Pretty.prune (d + 1) o Pretty.to_ML o Pretty.quote);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_ML o Pretty.position);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_ML o Pretty.mark_str o Path.print_markup);
+
+val _ =
+  ML_system_pp (fn _ => fn _ => fn t =>
+    ML_Pretty.str ("<thread " ^ quote (Isabelle_Thread.print t) ^
+      (if Isabelle_Thread.is_active t then "" else " (inactive)") ^ ">"));
+
+val _ =
+  ML_system_pp (fn _ => fn _ => fn bytes =>
+    ML_Pretty.str
+     (if Bytes.is_empty bytes then "Bytes.empty"
+      else "Bytes {size = " ^ string_of_int (Bytes.size bytes) ^ "}"));
diff -r 7d8b1ed1f748 -r 0f820da558f9 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Fri Sep 06 13:19:18 2024 +0200
+++ b/src/Pure/Isar/proof_display.ML	Fri Sep 06 13:49:43 2024 +0200
@@ -6,14 +6,6 @@
 
 signature PROOF_DISPLAY =
 sig
-  val pp_context: Proof.context -> Pretty.T
-  val guess_context: unit -> Proof.context
-  val pp_thm: thm -> Pretty.T
-  val pp_typ: typ -> Pretty.T
-  val pp_term: term -> Pretty.T
-  val pp_ctyp: ctyp -> Pretty.T
-  val pp_cterm: cterm -> Pretty.T
-  val pp_ztyp: ztyp -> Pretty.T
   val pretty_theory: bool -> Proof.context -> Pretty.T
   val pretty_definitions: bool -> Proof.context -> Pretty.T
   val pretty_theorems_diff: bool -> theory list -> Proof.context -> Pretty.T list
@@ -39,41 +31,6 @@
 structure Proof_Display: PROOF_DISPLAY =
 struct
 
-(** toplevel pretty printing **)
-
-fun pp_context ctxt =
- (if Config.get ctxt Proof_Context.debug then
-    Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
-  else Pretty.str "<context>");
-
-fun guess_context () =
-  let
-    fun global_context () =
-      Theory.get_pure ()
-      |> Config.put_global Name_Space.names_long true
-      |> Syntax.init_pretty_global;
-  in
-    (case Context.get_generic_context () of
-      SOME (Context.Proof ctxt) => ctxt
-    | SOME (Context.Theory thy) =>
-        (case try Syntax.init_pretty_global thy of
-          SOME ctxt => ctxt
-        | NONE => global_context ())
-    | NONE => global_context ())
-  end;
-
-fun pp_thm th = Thm.pretty_thm_raw (guess_context ()) {quote = true, show_hyps = false} th;
-
-fun pp_typ T = Pretty.quote (Syntax.pretty_typ (guess_context ()) T);
-fun pp_term t = Pretty.quote (Syntax.pretty_term (guess_context ()) t);
-
-val pp_ctyp = pp_typ o Thm.typ_of;
-val pp_cterm = pp_term o Thm.term_of;
-
-fun pp_ztyp T = Pretty.quote (Syntax.pretty_typ (guess_context ()) (ZTerm.typ_of T));
-
-
-
 (** theory content **)
 
 fun pretty_theory verbose ctxt =
diff -r 7d8b1ed1f748 -r 0f820da558f9 src/Pure/ML/ml_pp.ML
--- a/src/Pure/ML/ml_pp.ML	Fri Sep 06 13:19:18 2024 +0200
+++ b/src/Pure/ML/ml_pp.ML	Fri Sep 06 13:49:43 2024 +0200
@@ -4,42 +4,75 @@
 ML toplevel pretty-printing for logical entities.
 *)
 
+signature ML_PP =
+sig
+  val toplevel_context: unit -> Proof.context
+  val pp_context: Proof.context -> Pretty.T
+  val pp_typ: Proof.context -> typ -> Pretty.T
+  val pp_term: Proof.context -> term -> Pretty.T
+  val pp_thm: Proof.context -> thm -> Pretty.T
+end;
+
 structure ML_PP: sig end =
 struct
 
-val _ =
-  ML_system_pp (fn _ => fn _ => fn bytes =>
-    ML_Pretty.str
-     (if Bytes.is_empty bytes then "Bytes.empty"
-      else "Bytes {size = " ^ string_of_int (Bytes.size bytes) ^ "}"));
+(* logical context *)
 
-val _ =
-  ML_system_pp (fn _ => fn _ => Pretty.to_ML o Pretty.mark_str o Path.print_markup);
+(*ML compiler toplevel context: fallback on theory Pure for regular runtime*)
+fun toplevel_context () =
+  let
+    fun global_context () =
+      Theory.get_pure ()
+      |> Config.put_global Name_Space.names_long true
+      |> Syntax.init_pretty_global;
+  in
+    (case Context.get_generic_context () of
+      SOME (Context.Proof ctxt) => ctxt
+    | SOME (Context.Theory thy) =>
+        (case try Syntax.init_pretty_global thy of
+          SOME ctxt => ctxt
+        | NONE => global_context ())
+    | NONE => global_context ())
+  end;
 
-val _ =
-  ML_system_pp (fn _ => fn _ => fn t =>
-    ML_Pretty.str ("<thread " ^ quote (Isabelle_Thread.print t) ^
-      (if Isabelle_Thread.is_active t then "" else " (inactive)") ^ ">"));
+fun pp_context ctxt =
+ (if Config.get ctxt Proof_Context.debug then
+    Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
+  else Pretty.str "<context>");
+
+
+(* logical entities (with syntax) *)
+
+fun pp_typ ctxt T = Pretty.quote (Syntax.pretty_typ ctxt T);
+fun pp_term ctxt t = Pretty.quote (Syntax.pretty_term ctxt t);
+fun pp_thm ctxt th = Thm.pretty_thm_raw ctxt {quote = true, show_hyps = false} th;
 
 val _ =
-  ML_system_pp (fn _ => fn _ => Pretty.to_ML o Proof_Display.pp_context);
+  ML_system_pp (fn _ => fn _ => Pretty.to_ML o pp_context);
 
 val _ =
-  ML_system_pp (fn depth => fn _ => ML_Pretty.prune depth o Pretty.to_ML o Proof_Display.pp_thm);
+  ML_system_pp (fn depth => fn _ => fn th =>
+    ML_Pretty.prune depth (Pretty.to_ML (pp_thm (toplevel_context ()) th)));
 
 val _ =
-  ML_system_pp (fn depth => fn _ => ML_Pretty.prune depth o Pretty.to_ML o Proof_Display.pp_cterm);
+  ML_system_pp (fn depth => fn _ => fn ct =>
+    ML_Pretty.prune depth (Pretty.to_ML (pp_term (toplevel_context ()) (Thm.term_of ct))));
 
 val _ =
-  ML_system_pp (fn depth => fn _ => ML_Pretty.prune depth o Pretty.to_ML o Proof_Display.pp_ctyp);
+  ML_system_pp (fn depth => fn _ => fn cT =>
+    ML_Pretty.prune depth (Pretty.to_ML (pp_typ (toplevel_context ()) (Thm.typ_of cT))));
 
 val _ =
-  ML_system_pp (fn depth => fn _ => ML_Pretty.prune depth o Pretty.to_ML o Proof_Display.pp_typ);
+  ML_system_pp (fn depth => fn _ => fn T =>
+    ML_Pretty.prune depth (Pretty.to_ML (pp_typ (toplevel_context ()) T)));
 
 val _ =
-  ML_system_pp (fn depth => fn _ => ML_Pretty.prune depth o Pretty.to_ML o Proof_Display.pp_ztyp);
+  ML_system_pp (fn depth => fn _ => fn T =>
+    ML_Pretty.prune depth (Pretty.to_ML (pp_typ (toplevel_context ()) (ZTerm.typ_of T))));
 
 
+(* ML term and proofterm *)
+
 local
 
 fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
@@ -64,13 +97,6 @@
     | Var a => prt_app "Var" (Pretty.from_ML (ML_system_pretty (a, dp - 1)))
     | Bound a => prt_app "Bound" (Pretty.from_ML (ML_system_pretty (a, dp - 1))));
 
-in
-
-val _ = ML_system_pp (fn depth => fn _ => Pretty.to_ML o prt_term false depth);
-
-
-local
-
 fun prt_proof parens dp prf =
   if dp <= 0 then Pretty.str "..."
   else
@@ -113,11 +139,9 @@
 
 in
 
-val _ =
-  ML_system_pp (fn depth => fn _ => fn prf => Pretty.to_ML (prt_proof false depth prf));
+val _ = ML_system_pp (fn depth => fn _ => Pretty.to_ML o prt_term false depth);
+val _ = ML_system_pp (fn depth => fn _ => fn prf => Pretty.to_ML (prt_proof false depth prf));
 
 end;
 
 end;
-
-end;