# HG changeset patch
# User wenzelm
# Date 1305917043 -7200
# Node ID 6bc8a6dcb3e010f91e7c0bcd3f135658d9c7b7a9
# Parent  d96e53d0c638709fd5ae40a4a454f79d678f3ed8
added Isabelle_Process.is_active;
tuned signature;

diff -r d96e53d0c638 -r 6bc8a6dcb3e0 NEWS
--- 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.
 
diff -r d96e53d0c638 -r 6bc8a6dcb3e0 src/Pure/System/isabelle_process.ML
--- 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;