src/Pure/General/print_mode.ML
changeset 80861 9de19e3a7231
parent 62889 99c7f31615c2
child 80862 ab0234b9af65
--- a/src/Pure/General/print_mode.ML	Wed Sep 11 20:45:17 2024 +0200
+++ b/src/Pure/General/print_mode.ML	Wed Sep 11 21:25:15 2024 +0200
@@ -18,8 +18,9 @@
 sig
   include BASIC_PRINT_MODE
   val input: string
+  val internal: string
   val ASCII: string
-  val internal: string
+  val PIDE: string
   val setmp: string list -> ('a -> 'b) -> 'a -> 'b
   val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
   val closure: ('a -> 'b) -> 'a -> 'b
@@ -30,8 +31,9 @@
 struct
 
 val input = "input";
+val internal = "internal";
 val ASCII = "ASCII";
-val internal = "internal";
+val PIDE = "PIDE";
 
 val print_mode = Unsynchronized.ref ([]: string list);
 val print_mode_var = Thread_Data.var () : string list Thread_Data.var;