src/Pure/Tools/isabelle_process.ML

 
 signature ISABELLE_PROCESS =
 sig
   val test_markupN: string
   val test_markup: Markup.T -> output * output
+  val isabelle_processN: string
   val init: unit -> unit
 end;
 
 structure IsabelleProcess: ISABELLE_PROCESS =
 struct
 
-(* test markup *)
+(* test_markup *)
 
 val test_markupN = "test_markup";
 
 fun test_markup (name, props) =
  (enclose "<" ">" (space_implode " " (name :: map XML.attribute props)),

 
 val _ = Markup.add_mode test_markupN test_markup;
 
 
 (* channels *)
+
+val isabelle_processN = "isabelle_process";
 
 local
 
 fun special c = chr 2 ^ c;
 val special_end = special ".";

   Output.tracing_fn  := output "C" Markup.tracing;
   Output.warning_fn  := output "D" Markup.warning;
   Output.error_fn    := output "E" Markup.error;
   Output.debug_fn    := output "F" Markup.debug);
 
+val _ = Markup.add_mode isabelle_processN (fn (name, _) =>
+  if name = Markup.promptN then (special "G", special_end ^ "\n")
+  else ("", ""));
+
 end;
 
 
 (* init *)
 
 fun init () =
  (Output.writeln_default ("\nPID=" ^ string_of_pid (Posix.ProcEnv.getpid ()));
   setup_channels ();
+  change print_mode (update (op =) isabelle_processN);
   Isar.secure_main ());
 
 end;