added Isabelle_Process.is_active;
authorwenzelm
Fri May 20 20:44:03 2011 +0200 (2011-05-20 ago)
changeset 428976bc8a6dcb3e0
parent 42896 d96e53d0c638
child 42898 978b7ea3e3ee
added Isabelle_Process.is_active;
tuned signature;
NEWS
src/Pure/System/isabelle_process.ML
     1.1 --- a/NEWS	Fri May 20 18:12:12 2011 +0200
     1.2 +++ b/NEWS	Fri May 20 20:44:03 2011 +0200
     1.3 @@ -124,6 +124,10 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Isabelle_Process.is_active allows tools to check if the official
     1.8 +process wrapper is running (Isabelle/Scala/jEdit) or the old TTY loop
     1.9 +(better known as Proof General).
    1.10 +
    1.11  * Structure Proof_Context follows standard naming scheme.  Old
    1.12  ProofContext is still available for some time as legacy alias.
    1.13  
     2.1 --- a/src/Pure/System/isabelle_process.ML	Fri May 20 18:12:12 2011 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Fri May 20 20:44:03 2011 +0200
     2.3 @@ -17,7 +17,7 @@
     2.4  
     2.5  signature ISABELLE_PROCESS =
     2.6  sig
     2.7 -  val isabelle_processN: string
     2.8 +  val is_active: unit -> bool
     2.9    val add_command: string -> (string list -> unit) -> unit
    2.10    val command: string -> string list -> unit
    2.11    val crashes: exn list Unsynchronized.ref
    2.12 @@ -27,10 +27,12 @@
    2.13  structure Isabelle_Process: ISABELLE_PROCESS =
    2.14  struct
    2.15  
    2.16 -(* print modes *)
    2.17 +(* print mode *)
    2.18  
    2.19  val isabelle_processN = "isabelle_process";
    2.20  
    2.21 +fun is_active () = Print_Mode.print_mode_active isabelle_processN;
    2.22 +
    2.23  val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
    2.24  val _ = Markup.add_mode isabelle_processN YXML.output_markup;
    2.25