--- a/NEWS Fri May 20 18:12:12 2011 +0200
+++ b/NEWS Fri May 20 20:44:03 2011 +0200
@@ -124,6 +124,10 @@
*** ML ***
+* Isabelle_Process.is_active allows tools to check if the official
+process wrapper is running (Isabelle/Scala/jEdit) or the old TTY loop
+(better known as Proof General).
+
* Structure Proof_Context follows standard naming scheme. Old
ProofContext is still available for some time as legacy alias.
--- a/src/Pure/System/isabelle_process.ML Fri May 20 18:12:12 2011 +0200
+++ b/src/Pure/System/isabelle_process.ML Fri May 20 20:44:03 2011 +0200
@@ -17,7 +17,7 @@
signature ISABELLE_PROCESS =
sig
- val isabelle_processN: string
+ val is_active: unit -> bool
val add_command: string -> (string list -> unit) -> unit
val command: string -> string list -> unit
val crashes: exn list Unsynchronized.ref
@@ -27,10 +27,12 @@
structure Isabelle_Process: ISABELLE_PROCESS =
struct
-(* print modes *)
+(* print mode *)
val isabelle_processN = "isabelle_process";
+fun is_active () = Print_Mode.print_mode_active isabelle_processN;
+
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
val _ = Markup.add_mode isabelle_processN YXML.output_markup;