--- a/NEWS Mon Sep 20 11:55:36 2010 +0200
+++ b/NEWS Mon Sep 20 12:03:11 2010 +0200
@@ -244,6 +244,9 @@
*** ML ***
+* Discontinued Output.debug. Minor INCOMPATIBILITY, use plain writeln
+instead (or tracing for high-volume output).
+
* Configuration option show_question_marks only affects regular pretty
printing of types and terms, not raw Term.string_of_vname.
--- a/lib/Tools/mkfifo Mon Sep 20 11:55:36 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: create named pipe
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG"
- echo
- echo " Create a temporary named pipe and return its name."
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-## main
-
-[ "$#" != 0 ] && usage
-
-#FIXME potential race condition wrt. future processes with same pid
-FIFO="/tmp/isabelle-fifo$$"
-
-mkfifo -m 600 "$FIFO" || fail "Failed to create fifo: $FIFO"
-echo "$FIFO"
--- a/lib/Tools/rmfifo Mon Sep 20 11:55:36 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: remove named pipe
-
-
-PRG="$(basename "$0")"
-
-function usage()
-{
- echo
- echo "Usage: isabelle $PRG NAME"
- echo
- echo " Remove an unused named pipe, after producing dummy output"
- echo " to unblock the reader (blocks if no reader present)."
- echo
- exit 1
-}
-
-
-## main
-
-[ "$#" != 1 ] && usage
-FIFO="$1"; shift
-
-if [ -p "$FIFO" ]; then
- echo -n "" >"$FIFO" && rm -f "$FIFO"
-fi
--- a/src/Pure/General/antiquote.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/General/antiquote.ML Mon Sep 20 12:03:11 2010 +0200
@@ -36,7 +36,7 @@
(* report *)
-val report_antiq = Position.report Markup.antiq;
+fun report_antiq pos = Position.report pos Markup.antiq;
fun report report_text (Text x) = report_text x
| report _ (Antiq (_, (pos, _))) = report_antiq pos
--- a/src/Pure/General/markup.scala Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/General/markup.scala Mon Sep 20 12:03:11 2010 +0200
@@ -235,19 +235,15 @@
val INIT = "init"
val STATUS = "status"
+ val REPORT = "report"
val WRITELN = "writeln"
val TRACING = "tracing"
val WARNING = "warning"
val ERROR = "error"
- val DEBUG = "debug"
val SYSTEM = "system"
- val INPUT = "input"
- val STDIN = "stdin"
val STDOUT = "stdout"
- val SIGNAL = "signal"
val EXIT = "exit"
- val REPORT = "report"
val NO_REPORT = "no_report"
val BAD = "bad"
--- a/src/Pure/General/position.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/General/position.ML Mon Sep 20 12:03:11 2010 +0200
@@ -28,9 +28,9 @@
val properties_of: T -> Properties.T
val default_properties: T -> Properties.T -> Properties.T
val markup: T -> Markup.T -> Markup.T
- val reported_text: Markup.T -> T -> string -> string
- val report_text: Markup.T -> T -> string -> unit
- val report: Markup.T -> T -> unit
+ val reported_text: T -> Markup.T -> string -> string
+ val report_text: T -> Markup.T -> string -> unit
+ val report: T -> Markup.T -> unit
val str_of: T -> string
type range = T * T
val no_range: range
@@ -132,12 +132,12 @@
(* reports *)
-fun reported_text m (pos as Pos (count, _)) txt =
+fun reported_text (pos as Pos (count, _)) m txt =
if invalid_count count then ""
else Markup.markup (markup pos m) txt;
-fun report_text markup pos txt = Output.report (reported_text markup pos txt);
-fun report markup pos = report_text markup pos "";
+fun report_text pos markup txt = Output.report (reported_text pos markup txt);
+fun report pos markup = report_text pos markup "";
(* str_of *)
--- a/src/Pure/Isar/attrib.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Mon Sep 20 12:03:11 2010 +0200
@@ -108,7 +108,7 @@
let val ((name, _), pos) = Args.dest_src src in
(case Symtab.lookup attrs name of
NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
- | SOME (att, _) => (Position.report (Markup.attribute name) pos; att src))
+ | SOME (att, _) => (Position.report pos (Markup.attribute name); att src))
end;
in attr end;
--- a/src/Pure/Isar/isar_cmd.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Mon Sep 20 12:03:11 2010 +0200
@@ -494,7 +494,7 @@
(* markup commands *)
fun check_text (txt, pos) state =
- (Position.report Markup.doc_source pos;
+ (Position.report pos Markup.doc_source;
ignore (Thy_Output.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
fun header_markup txt = Toplevel.keep (fn state =>
--- a/src/Pure/Isar/method.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/Isar/method.ML Mon Sep 20 12:03:11 2010 +0200
@@ -358,7 +358,7 @@
let val ((name, _), pos) = Args.dest_src src in
(case Symtab.lookup meths name of
NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
- | SOME (mth, _) => (Position.report (Markup.method name) pos; mth src))
+ | SOME (mth, _) => (Position.report pos (Markup.method name); mth src))
end;
in meth end;
--- a/src/Pure/Isar/proof_context.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Sep 20 12:03:11 2010 +0200
@@ -333,7 +333,7 @@
val (syms, pos) = Syntax.read_token text;
val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
- val _ = Context_Position.report ctxt (Markup.tclass c) pos;
+ val _ = Context_Position.report ctxt pos (Markup.tclass c);
in c end;
@@ -467,7 +467,7 @@
val _ =
if strict then ignore (Consts.the_type consts d) handle TYPE (msg, _, _) => err msg
else ();
- val _ = Context_Position.report ctxt (Markup.const d) pos;
+ val _ = Context_Position.report ctxt pos (Markup.const d);
in t end;
in
@@ -478,13 +478,13 @@
val (c, pos) = token_content text;
in
if Syntax.is_tid c then
- (Context_Position.report ctxt Markup.tfree pos;
+ (Context_Position.report ctxt pos Markup.tfree;
TFree (c, default_sort ctxt (c, ~1)))
else
let
val d = Type.intern_type tsig c;
val decl = Type.the_decl tsig d;
- val _ = Context_Position.report ctxt (Markup.tycon d) pos;
+ val _ = Context_Position.report ctxt pos (Markup.tycon d);
fun err () = error ("Bad type name: " ^ quote d);
val args =
(case decl of
@@ -509,8 +509,8 @@
in
(case (lookup_skolem ctxt c, Variable.is_const ctxt c) of
(SOME x, false) =>
- (Context_Position.report ctxt (Markup.name x
- (if can Name.dest_skolem x then Markup.skolem else Markup.free)) pos;
+ (Context_Position.report ctxt pos
+ (Markup.name x (if can Name.dest_skolem x then Markup.skolem else Markup.free));
Free (x, infer_type ctxt (x, ty)))
| _ => prep_const_proper ctxt strict (c, pos))
end;
@@ -585,17 +585,17 @@
local
-structure Allow_Dummies = Proof_Data(type T = bool fun init _ = false);
+val dummies = Config.bool (Config.declare "ProofContext.dummies" (K (Config.Bool false)));
fun check_dummies ctxt t =
- if Allow_Dummies.get ctxt then t
+ if Config.get ctxt dummies then t
else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term";
fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1);
in
-val allow_dummies = Allow_Dummies.put true;
+val allow_dummies = Config.put dummies true;
fun prepare_patterns ctxt =
let val Mode {pattern, ...} = get_mode ctxt in
@@ -735,7 +735,7 @@
fun parse_failed ctxt pos msg kind =
cat_error msg ("Failed to parse " ^ kind ^
- Markup.markup Markup.report (Context_Position.reported_text ctxt Markup.bad pos ""));
+ Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
fun parse_sort ctxt text =
let
@@ -979,7 +979,8 @@
if name = "" then [Thm.transfer thy Drule.dummy_thm]
else
(case Facts.lookup (Context.Proof ctxt) local_facts name of
- SOME (_, ths) => (Context_Position.report ctxt (Markup.local_fact name) pos;
+ SOME (_, ths) =>
+ (Context_Position.report ctxt pos (Markup.local_fact name);
map (Thm.transfer thy) (Facts.select thmref ths))
| NONE => PureThy.get_fact (Context.Proof ctxt) thy xthmref);
in pick name thms end;
@@ -1009,7 +1010,7 @@
let
val pos = Binding.pos_of b;
val name = full_name ctxt b;
- val _ = Context_Position.report ctxt (Markup.local_fact_decl name) pos;
+ val _ = Context_Position.report ctxt pos (Markup.local_fact_decl name);
val facts = PureThy.name_thmss false name raw_facts;
fun app (th, attrs) x =
@@ -1188,7 +1189,7 @@
|> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
|-> (map_syntax o Local_Syntax.add_syntax (theory_of ctxt) o map (pair Local_Syntax.Fixed));
val _ = (vars ~~ xs') |> List.app (fn ((b, _, _), x') =>
- Context_Position.report ctxt (Markup.fixed_decl x') (Binding.pos_of b));
+ Context_Position.report ctxt (Binding.pos_of b) (Markup.fixed_decl x'));
in (xs', ctxt'') end;
--- a/src/Pure/Isar/runtime.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/Isar/runtime.ML Mon Sep 20 12:03:11 2010 +0200
@@ -10,6 +10,7 @@
exception TERMINATE
exception EXCURSION_FAIL of exn * string
exception TOPLEVEL_ERROR
+ val debug: bool Unsynchronized.ref
val exn_context: Proof.context option -> exn -> exn
val exn_messages: (exn -> Position.T) -> exn -> string list
val exn_message: (exn -> Position.T) -> exn -> string
@@ -28,6 +29,8 @@
exception EXCURSION_FAIL of exn * string;
exception TOPLEVEL_ERROR;
+val debug = Unsynchronized.ref false;
+
(* exn_context *)
@@ -52,7 +55,7 @@
| _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
end;
- val detailed = ! Output.debugging;
+ val detailed = ! debug;
fun exn_msgs context exn =
if Exn.is_interrupt exn then []
@@ -94,11 +97,10 @@
| msgs => cat_lines msgs);
-
(** controlled execution **)
fun debugging f x =
- if ! Output.debugging then
+ if ! debug then
Exn.release (exception_trace (fn () =>
Exn.Result (f x) handle
exn as UNDEF => Exn.Exn exn
--- a/src/Pure/Isar/toplevel.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Mon Sep 20 12:03:11 2010 +0200
@@ -215,7 +215,7 @@
(** toplevel transitions **)
val quiet = Unsynchronized.ref false;
-val debug = Output.debugging;
+val debug = Runtime.debug;
val interact = Unsynchronized.ref false;
val timing = Output.timing;
val profiling = Unsynchronized.ref 0;
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Mon Sep 20 12:03:11 2010 +0200
@@ -48,12 +48,12 @@
| _ => Position.report_text);
fun report_decl markup loc decl =
- report_text Markup.ML_ref (offset_position_of loc)
+ report_text (offset_position_of loc) Markup.ML_ref
(Markup.markup (Position.markup (position_of decl) markup) "");
fun report loc (PolyML.PTtype types) =
PolyML.NameSpace.displayTypeExpression (types, depth, space)
|> pretty_ml |> Pretty.from_ML |> Pretty.string_of
- |> report_text Markup.ML_typing (offset_position_of loc)
+ |> report_text (offset_position_of loc) Markup.ML_typing
| report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl
| report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl
| report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl
@@ -124,7 +124,7 @@
Markup.markup Markup.no_report
((if hard then "Error" else "Warning") ^ Position.str_of (position_of loc) ^ ":\n") ^
Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
- Position.reported_text Markup.report (offset_position_of loc) "";
+ Position.reported_text (offset_position_of loc) Markup.report "";
in if hard then err txt else warn txt end;
--- a/src/Pure/ML/ml_context.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/ML/ml_context.ML Mon Sep 20 12:03:11 2010 +0200
@@ -118,7 +118,8 @@
let val ((name, _), pos) = Args.dest_src src in
(case Symtab.lookup (! global_parsers) name of
NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
- | SOME scan => (Context_Position.report ctxt (Markup.ML_antiq name) pos;
+ | SOME scan =>
+ (Context_Position.report ctxt pos (Markup.ML_antiq name);
Args.context_syntax "ML antiquotation" (scan pos) src ctxt))
end;
--- a/src/Pure/ML/ml_lex.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/ML/ml_lex.ML Mon Sep 20 12:03:11 2010 +0200
@@ -112,7 +112,7 @@
in
-fun report_token (Token ((pos, _), (kind, x))) = Position.report (token_markup kind x) pos;
+fun report_token (Token ((pos, _), (kind, x))) = Position.report pos (token_markup kind x);
end;
@@ -265,7 +265,7 @@
fun read pos txt =
let
- val _ = Position.report Markup.ML_source pos;
+ val _ = Position.report pos Markup.ML_source;
val syms = Symbol_Pos.explode (txt, pos);
val termination =
if null syms then []
--- a/src/Pure/ML/ml_syntax.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/ML/ml_syntax.ML Mon Sep 20 12:03:11 2010 +0200
@@ -62,6 +62,9 @@
if not (Symbol.is_char s) then s
else if s = "\"" then "\\\""
else if s = "\\" then "\\\\"
+ else if s = "\t" then "\\t"
+ else if s = "\n" then "\\n"
+ else if s = "\r" then "\\r"
else
let val c = ord s in
if c < 32 then "\\^" ^ chr (c + ord "@")
--- a/src/Pure/PIDE/isar_document.scala Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala Mon Sep 20 12:03:11 2010 +0200
@@ -70,7 +70,19 @@
}
- /* reported positions */
+ /* specific messages */
+
+ def is_warning(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.WARNING, _), _) => true
+ case _ => false
+ }
+
+ def is_error(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.ERROR, _), _) => true
+ case _ => false
+ }
def is_state(msg: XML.Tree): Boolean =
msg match {
@@ -78,6 +90,9 @@
case _ => false
}
+
+ /* reported positions */
+
private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Mon Sep 20 12:03:11 2010 +0200
@@ -79,7 +79,6 @@
Output.report_fn := (fn _ => ());
Output.priority_fn := message (special "I") (special "J") "";
Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
- Output.debug_fn := message (special "K") (special "L") "+++ ";
Output.warning_fn := message (special "K") (special "L") "### ";
Output.error_fn := message (special "M") (special "N") "*** ";
Output.prompt_fn := (fn s => Output.std_output (render s ^ special "S")));
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Sep 20 12:03:11 2010 +0200
@@ -166,8 +166,7 @@
Output.priority_fn := (fn s => normalmsg Status s);
Output.tracing_fn := (fn s => normalmsg Tracing s);
Output.warning_fn := (fn s => errormsg Message Warning s);
- Output.error_fn := (fn s => errormsg Message Fatal s);
- Output.debug_fn := (fn s => errormsg Message Debug s));
+ Output.error_fn := (fn s => errormsg Message Fatal s));
(* immediate messages *)
--- a/src/Pure/ROOT.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/ROOT.ML Mon Sep 20 12:03:11 2010 +0200
@@ -96,13 +96,13 @@
use "old_term.ML";
use "General/pretty.ML";
use "context.ML";
+use "config.ML";
use "context_position.ML";
use "sorts.ML";
use "type.ML";
use "logic.ML";
use "Syntax/lexicon.ML";
use "Syntax/simple_syntax.ML";
-use "config.ML";
(* inner syntax *)
--- a/src/Pure/Syntax/lexicon.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/Syntax/lexicon.ML Mon Sep 20 12:03:11 2010 +0200
@@ -66,7 +66,7 @@
val terminals: string list
val is_terminal: string -> bool
val report_token: Proof.context -> token -> unit
- val report_token_range: Proof.context -> token -> unit
+ val reported_token_range: Proof.context -> token -> string
val matching_tokens: token * token -> bool
val valued_token: token -> bool
val predef_term: string -> token option
@@ -187,12 +187,12 @@
| EOF => Markup.empty;
fun report_token ctxt (Token (kind, _, (pos, _))) =
- Context_Position.report ctxt (token_kind_markup kind) pos;
+ Context_Position.report ctxt pos (token_kind_markup kind);
-fun report_token_range ctxt tok =
+fun reported_token_range ctxt tok =
if is_proper tok
- then Context_Position.report ctxt Markup.token_range (pos_of_token tok)
- else ();
+ then Context_Position.reported_text ctxt (pos_of_token tok) Markup.token_range ""
+ else "";
(* matching_tokens *)
--- a/src/Pure/Syntax/syntax.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML Mon Sep 20 12:03:11 2010 +0200
@@ -182,7 +182,7 @@
fun parse_token ctxt markup str =
let
val (syms, pos) = read_token str;
- val _ = Context_Position.report ctxt markup pos;
+ val _ = Context_Position.report ctxt pos markup;
in (syms, pos) end;
local
@@ -361,9 +361,9 @@
(* global pretty printing *)
-structure PrettyGlobal = Proof_Data(type T = bool fun init _ = false);
-val is_pretty_global = PrettyGlobal.get;
-val set_pretty_global = PrettyGlobal.put;
+val pretty_global = Config.bool (Config.declare "Syntax.pretty_global" (K (Config.Bool false)));
+fun is_pretty_global ctxt = Config.get ctxt pretty_global;
+val set_pretty_global = Config.put pretty_global;
val init_pretty_global = set_pretty_global true o ProofContext.init_global;
val pretty_term_global = pretty_term o init_pretty_global;
@@ -710,7 +710,9 @@
val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks)
- handle ERROR msg => (List.app (Lexicon.report_token_range ctxt) toks; error msg);
+ handle ERROR msg =>
+ error (msg ^
+ implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
val len = length pts;
val limit = Config.get ctxt ambiguity_limit;
--- a/src/Pure/System/isabelle_process.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML Mon Sep 20 12:03:11 2010 +0200
@@ -3,6 +3,16 @@
Isabelle process wrapper, based on private fifos for maximum
robustness and performance.
+
+Startup phases:
+ . raw Posix process startup with uncontrolled output on stdout/stderr
+ . stdout \002: ML running
+ .. stdin/stdout/stderr freely available (raw ML loop)
+ .. protocol thread initialization
+ ... switch to in_fifo/out_fifo channels (rendezvous via open)
+ ... out_fifo INIT(pid): channels ready
+ ... out_fifo STATUS(keywords)
+ ... out_fifo READY: main loop ready
*)
signature ISABELLE_PROCESS =
@@ -62,9 +72,10 @@
in
-fun standard_message out_stream ch body =
+fun standard_message out_stream with_serial ch body =
message out_stream ch
- ((Markup.serialN, serial_string ()) :: Position.properties_of (Position.thread_data ())) body;
+ ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
+ (Position.properties_of (Position.thread_data ()))) body;
fun init_message out_stream =
message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());
@@ -83,32 +94,24 @@
(OS.Process.sleep (Time.fromMilliseconds 20); try TextIO.flushOut stream; loop ());
in loop end;
-fun rendezvous f fifo =
- let
- val path = File.platform_path (Path.explode fifo);
- val result = f fifo; (*should block until peer is ready*)
- val _ =
- if String.isSuffix "cygwin" ml_platform then () (*Cygwin 1.7: no proper blocking on open*)
- else OS.FileSys.remove path; (*prevent future access*)
- in result end;
-
in
fun setup_channels in_fifo out_fifo =
let
- val in_stream = rendezvous TextIO.openIn in_fifo;
- val out_stream = rendezvous TextIO.openOut out_fifo;
+ (*rendezvous*)
+ val in_stream = TextIO.openIn in_fifo;
+ val out_stream = TextIO.openOut out_fifo;
+
val _ = Simple_Thread.fork false (auto_flush out_stream);
val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
in
- Output.status_fn := standard_message out_stream "B";
- Output.report_fn := standard_message out_stream "C";
- Output.writeln_fn := standard_message out_stream "D";
- Output.tracing_fn := standard_message out_stream "E";
- Output.warning_fn := standard_message out_stream "F";
- Output.error_fn := standard_message out_stream "G";
- Output.debug_fn := standard_message out_stream "H";
+ Output.status_fn := standard_message out_stream false "B";
+ Output.report_fn := standard_message out_stream false "C";
+ Output.writeln_fn := standard_message out_stream true "D";
+ Output.tracing_fn := standard_message out_stream true "E";
+ Output.warning_fn := standard_message out_stream true "F";
+ Output.error_fn := standard_message out_stream true "G";
Output.priority_fn := ! Output.writeln_fn;
Output.prompt_fn := ignore;
(in_stream, out_stream)
@@ -166,17 +169,21 @@
(* init *)
-fun init in_fifo out_fifo =
+fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
let
+ val _ = OS.Process.sleep (Time.fromMilliseconds 500); (*yield to raw ML toplevel*)
+ val _ = Output.std_output Symbol.STX;
+
+ val _ = quick_and_dirty := true; (* FIXME !? *)
+ val _ = Context.set_thread_data NONE;
val _ = Unsynchronized.change print_mode
(fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
+
val (in_stream, out_stream) = setup_channels in_fifo out_fifo;
val _ = init_message out_stream;
- val _ = quick_and_dirty := true; (* FIXME !? *)
val _ = Keyword.status ();
val _ = Output.status (Markup.markup Markup.ready "");
- val _ = Context.set_thread_data NONE;
- val _ = Simple_Thread.fork false (fn () => (loop in_stream; quit ()));
- in () end;
+ in loop in_stream end));
end;
+
--- a/src/Pure/System/isabelle_process.scala Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala Mon Sep 20 12:03:11 2010 +0200
@@ -19,30 +19,16 @@
{
/* results */
- object Kind {
- // message markup
- val markup = Map(
+ object Kind
+ {
+ val message_markup = Map(
('A' : Int) -> Markup.INIT,
('B' : Int) -> Markup.STATUS,
('C' : Int) -> Markup.REPORT,
('D' : Int) -> Markup.WRITELN,
('E' : Int) -> Markup.TRACING,
('F' : Int) -> Markup.WARNING,
- ('G' : Int) -> Markup.ERROR,
- ('H' : Int) -> Markup.DEBUG)
- def is_raw(kind: String) =
- kind == Markup.STDOUT
- def is_control(kind: String) =
- kind == Markup.SYSTEM ||
- kind == Markup.SIGNAL ||
- kind == Markup.EXIT
- def is_system(kind: String) =
- kind == Markup.SYSTEM ||
- kind == Markup.INPUT ||
- kind == Markup.STDIN ||
- kind == Markup.SIGNAL ||
- kind == Markup.EXIT ||
- kind == Markup.STATUS
+ ('G' : Int) -> Markup.ERROR)
}
class Result(val message: XML.Elem)
@@ -51,9 +37,10 @@
def properties = message.markup.properties
def body = message.body
- def is_raw = Kind.is_raw(kind)
- def is_control = Kind.is_control(kind)
- def is_system = Kind.is_system(kind)
+ def is_init = kind == Markup.INIT
+ def is_exit = kind == Markup.EXIT
+ def is_stdout = kind == Markup.STDOUT
+ def is_system = kind == Markup.SYSTEM
def is_status = kind == Markup.STATUS
def is_report = kind == Markup.REPORT
def is_ready = is_status && body == List(XML.Elem(Markup.Ready, Nil))
@@ -73,7 +60,7 @@
}
-class Isabelle_Process(system: Isabelle_System, receiver: Actor, args: String*)
+class Isabelle_Process(system: Isabelle_System, timeout: Int, receiver: Actor, args: String*)
{
import Isabelle_Process._
@@ -81,24 +68,107 @@
/* demo constructor */
def this(args: String*) =
- this(new Isabelle_System,
+ this(new Isabelle_System, 10000,
actor { loop { react { case res => Console.println(res) } } }, args: _*)
- /* process information */
+ /* input actors */
+
+ private case class Input_Text(text: String)
+ private case class Input_Chunks(chunks: List[Array[Byte]])
+
+ private case object Close
+ private def close(a: Actor) { if (a != null) a ! Close }
+
+ @volatile private var standard_input: Actor = null
+ @volatile private var command_input: Actor = null
+
+
+ /* process manager */
+
+ private val in_fifo = system.mk_fifo()
+ private val out_fifo = system.mk_fifo()
+ private def rm_fifos() { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
+
+ private val proc =
+ try {
+ val cmdline =
+ List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
+ system.execute(true, cmdline: _*)
+ }
+ catch { case e: IOException => rm_fifos(); throw(e) }
+
+ private val stdout_reader =
+ new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
+
+ private val stdin_writer =
+ new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
+
+ Simple_Thread.actor("process_manager") {
+ val (startup_failed, startup_output) =
+ {
+ val expired = System.currentTimeMillis() + timeout
+ val result = new StringBuilder(100)
- @volatile private var proc: Option[Process] = None
- @volatile private var pid: Option[String] = None
+ var finished = false
+ while (!finished && System.currentTimeMillis() <= expired) {
+ while (!finished && stdout_reader.ready) {
+ val c = stdout_reader.read
+ if (c == 2) finished = true
+ else result += c.toChar
+ }
+ Thread.sleep(10)
+ }
+ (!finished, result.toString)
+ }
+ if (startup_failed) {
+ put_result(Markup.STDOUT, startup_output)
+ put_result(Markup.EXIT, "127")
+ stdin_writer.close
+ Thread.sleep(300) // FIXME !?
+ proc.destroy // FIXME reliable!?
+ }
+ else {
+ put_result(Markup.SYSTEM, startup_output)
+
+ standard_input = stdin_actor()
+ stdout_actor()
+
+ // rendezvous
+ val command_stream = system.fifo_output_stream(in_fifo)
+ val message_stream = system.fifo_input_stream(out_fifo)
+
+ command_input = input_actor(command_stream)
+ message_actor(message_stream)
+
+ val rc = proc.waitFor()
+ Thread.sleep(300) // FIXME !?
+ system_result("Isabelle process terminated")
+ put_result(Markup.EXIT, rc.toString)
+ }
+ rm_fifos()
+ }
/* results */
+ private def system_result(text: String)
+ {
+ receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
+ }
+
+
private val xml_cache = new XML.Cache(131071)
private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
{
- if (pid.isEmpty && kind == Markup.INIT)
- pid = props.find(_._1 == Markup.PID).map(_._1)
+ if (pid.isEmpty && kind == Markup.INIT) {
+ rm_fifos()
+ props.find(_._1 == Markup.PID).map(_._1) match {
+ case None => system_result("Bad Isabelle process initialization: missing pid")
+ case p => pid = p
+ }
+ }
val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
xml_cache.cache_tree(msg)((message: XML.Tree) =>
@@ -113,34 +183,33 @@
/* signals */
+ @volatile private var pid: Option[String] = None
+
def interrupt()
{
- if (proc.isEmpty) put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: no process")
- else
- pid match {
- case None => put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: unknowd pid")
- case Some(i) =>
- try {
- if (system.execute(true, "kill", "-INT", i).waitFor == 0)
- put_result(Markup.SIGNAL, "INT")
- else
- put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: kill command failed")
- }
- catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
- }
+ pid match {
+ case None => system_result("Cannot interrupt Isabelle: unknowd pid")
+ case Some(i) =>
+ try {
+ if (system.execute(true, "kill", "-INT", i).waitFor == 0)
+ system_result("Interrupt Isabelle")
+ else
+ system_result("Cannot interrupt Isabelle: kill command failed")
+ }
+ catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
+ }
}
def kill()
{
- proc match {
- case None => put_result(Markup.SYSTEM, "Cannot kill Isabelle: no process")
- case Some(p) =>
- close()
- Thread.sleep(500) // FIXME !?
- put_result(Markup.SIGNAL, "KILL")
- p.destroy
- proc = None
- pid = None
+ val running =
+ try { proc.exitValue; false }
+ catch { case e: java.lang.IllegalThreadStateException => true }
+ if (running) {
+ close()
+ Thread.sleep(500) // FIXME !?
+ system_result("Kill Isabelle")
+ proc.destroy
}
}
@@ -148,45 +217,40 @@
/** stream actors **/
- case class Input_Text(text: String)
- case class Input_Chunks(chunks: List[Array[Byte]])
- case object Close
-
-
/* raw stdin */
- private def stdin_actor(name: String, stream: OutputStream): Actor =
+ private def stdin_actor(): Actor =
+ {
+ val name = "standard_input"
Simple_Thread.actor(name) {
- val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset))
var finished = false
while (!finished) {
try {
//{{{
receive {
case Input_Text(text) =>
- // FIXME echo input?!
- writer.write(text)
- writer.flush
+ stdin_writer.write(text)
+ stdin_writer.flush
case Close =>
- writer.close
+ stdin_writer.close
finished = true
case bad => System.err.println(name + ": ignoring bad message " + bad)
}
//}}}
}
- catch {
- case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
- }
+ catch { case e: IOException => system_result(name + ": " + e.getMessage) }
}
- put_result(Markup.SYSTEM, name + " terminated")
+ system_result(name + " terminated")
}
+ }
/* raw stdout */
- private def stdout_actor(name: String, stream: InputStream): Actor =
+ private def stdout_actor(): Actor =
+ {
+ val name = "standard_output"
Simple_Thread.actor(name) {
- val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
var result = new StringBuilder(100)
var finished = false
@@ -195,8 +259,8 @@
//{{{
var c = -1
var done = false
- while (!done && (result.length == 0 || reader.ready)) {
- c = reader.read
+ while (!done && (result.length == 0 || stdout_reader.ready)) {
+ c = stdout_reader.read
if (c >= 0) result.append(c.asInstanceOf[Char])
else done = true
}
@@ -205,23 +269,23 @@
result.length = 0
}
else {
- reader.close
+ stdout_reader.close
finished = true
- close()
}
//}}}
}
- catch {
- case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
- }
+ catch { case e: IOException => system_result(name + ": " + e.getMessage) }
}
- put_result(Markup.SYSTEM, name + " terminated")
+ system_result(name + " terminated")
}
+ }
/* command input */
- private def input_actor(name: String, raw_stream: OutputStream): Actor =
+ private def input_actor(raw_stream: OutputStream): Actor =
+ {
+ val name = "command_input"
Simple_Thread.actor(name) {
val stream = new BufferedOutputStream(raw_stream)
var finished = false
@@ -241,19 +305,21 @@
}
//}}}
}
- catch {
- case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
- }
+ catch { case e: IOException => system_result(name + ": " + e.getMessage) }
}
- put_result(Markup.SYSTEM, name + " terminated")
+ system_result(name + " terminated")
}
+ }
/* message output */
- private class Protocol_Error(msg: String) extends Exception(msg)
+ private def message_actor(stream: InputStream): Actor =
+ {
+ class EOF extends Exception
+ class Protocol_Error(msg: String) extends Exception(msg)
- private def message_actor(name: String, stream: InputStream): Actor =
+ val name = "message_output"
Simple_Thread.actor(name) {
val default_buffer = new Array[Byte](65536)
var c = -1
@@ -264,6 +330,7 @@
// chunk size
var n = 0
c = stream.read
+ if (c == -1) throw new EOF
while (48 <= c && c <= 57) {
n = 10 * n + (c - 48)
c = stream.read
@@ -294,71 +361,24 @@
val body = read_chunk()
header match {
case List(XML.Elem(Markup(name, props), Nil))
- if name.size == 1 && Kind.markup.isDefinedAt(name(0)) =>
- put_result(Kind.markup(name(0)), props, body)
+ if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
+ put_result(Kind.message_markup(name(0)), props, body)
case _ => throw new Protocol_Error("bad header: " + header.toString)
}
}
catch {
- case e: IOException =>
- put_result(Markup.SYSTEM, "Cannot read message:\n" + e.getMessage)
- case e: Protocol_Error =>
- put_result(Markup.SYSTEM, "Malformed message:\n" + e.getMessage)
+ case e: IOException => system_result("Cannot read message:\n" + e.getMessage)
+ case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage)
+ case _: EOF =>
}
} while (c != -1)
stream.close
- close()
- put_result(Markup.SYSTEM, name + " terminated")
+ system_result(name + " terminated")
}
-
-
-
- /** init **/
-
- /* exec process */
-
- private val in_fifo = system.mk_fifo()
- private val out_fifo = system.mk_fifo()
- private def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
-
- try {
- val cmdline =
- List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
- proc = Some(system.execute(true, cmdline: _*))
- }
- catch {
- case e: IOException =>
- rm_fifos()
- error("Failed to execute Isabelle process: " + e.getMessage)
}
- /* I/O actors */
-
- private val standard_input = stdin_actor("standard_input", proc.get.getOutputStream)
- stdout_actor("standard_output", proc.get.getInputStream)
-
- private val command_input = input_actor("command_input", system.fifo_output_stream(in_fifo))
- message_actor("message_output", system.fifo_input_stream(out_fifo))
-
-
- /* exit process */
-
- Simple_Thread.actor("process_exit") {
- proc match {
- case None =>
- case Some(p) =>
- val rc = p.waitFor()
- Thread.sleep(300) // FIXME property!?
- put_result(Markup.SYSTEM, "process_exit terminated")
- put_result(Markup.EXIT, rc.toString)
- }
- rm_fifos()
- }
-
-
-
/** main methods **/
def input_raw(text: String): Unit = standard_input ! Input_Text(text)
@@ -369,5 +389,5 @@
def input(name: String, args: String*): Unit =
input_bytes(name, args.map(Standard_System.string_bytes): _*)
- def close(): Unit = command_input ! Close
+ def close(): Unit = { close(command_input); close(standard_input) }
}
--- a/src/Pure/System/isabelle_system.scala Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala Mon Sep 20 12:03:11 2010 +0200
@@ -273,17 +273,28 @@
/* named pipes */
+ private var fifo_count: Long = 0
+ private def next_fifo(): String = synchronized {
+ require(fifo_count < java.lang.Long.MAX_VALUE)
+ fifo_count += 1
+ fifo_count.toString
+ }
+
def mk_fifo(): String =
{
- val (result, rc) = isabelle_tool("mkfifo")
- if (rc == 0) result.trim
+ val i = next_fifo()
+ val script =
+ "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$-" + i + "\"\n" +
+ "mkfifo -m 600 \"$FIFO\" || { echo \"Failed to create fifo: $FIFO\" >&2; exit 2; }\n" +
+ "echo -n \"$FIFO\"\n"
+ val (result, rc) = bash_output(script)
+ if (rc == 0) result
else error(result)
}
def rm_fifo(fifo: String)
{
- val (result, rc) = isabelle_tool("rmfifo", fifo)
- if (rc != 0) error(result)
+ bash_output("rm -f '" + fifo + "'")
}
def fifo_input_stream(fifo: String): InputStream =
--- a/src/Pure/System/session.scala Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/System/session.scala Mon Sep 20 12:03:11 2010 +0200
@@ -200,8 +200,8 @@
case _ => if (!result.is_ready) bad_result(result)
}
}
- else if (result.kind == Markup.EXIT) prover = null
- else if (result.is_raw) raw_output.event(result)
+ else if (result.is_exit) prover = null // FIXME ??
+ else if (result.is_stdout) raw_output.event(result)
else if (!result.is_system) bad_result(result) // FIXME syslog for system messages (!?)
}
}
@@ -216,7 +216,7 @@
while (
receiveWithin(0) {
case result: Isabelle_Process.Result =>
- if (result.is_raw) {
+ if (result.is_stdout) {
for (text <- XML.content(result.message))
buf.append(text)
}
@@ -229,16 +229,14 @@
def prover_startup(timeout: Int): Option[String] =
{
receiveWithin(timeout) {
- case result: Isabelle_Process.Result
- if result.kind == Markup.INIT =>
+ case result: Isabelle_Process.Result if result.is_init =>
while (receive {
case result: Isabelle_Process.Result =>
handle_result(result); !result.is_ready
}) {}
None
- case result: Isabelle_Process.Result
- if result.kind == Markup.EXIT =>
+ case result: Isabelle_Process.Result if result.is_exit =>
Some(startup_error())
case TIMEOUT => // FIXME clarify
@@ -247,7 +245,7 @@
}
- /* main loop */
+ /* main loop */ // FIXME proper shutdown
var finished = false
while (!finished) {
@@ -272,7 +270,7 @@
case Started(timeout, args) =>
if (prover == null) {
- prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
+ prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
val origin = sender
val opt_err = prover_startup(timeout)
if (opt_err.isDefined) prover = null
@@ -282,9 +280,9 @@
case Stop => // FIXME synchronous!?
if (prover != null) {
+ global_state.change(_ => Document.State.init)
prover.kill
prover = null
- finished = true
}
case TIMEOUT => // FIXME clarify
--- a/src/Pure/System/standard_system.scala Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/System/standard_system.scala Mon Sep 20 12:03:11 2010 +0200
@@ -132,9 +132,7 @@
for ((x, y) <- env) proc.environment.put(x, y)
}
proc.redirectErrorStream(redirect)
-
- try { proc.start }
- catch { case e: IOException => error(e.getMessage) }
+ proc.start
}
def process_output(proc: Process): (String, Int) =
@@ -152,8 +150,8 @@
(output, rc)
}
- def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*):
- (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
+ def raw_exec(cwd: File, env: Map[String, String], redirect: Boolean, args: String*)
+ : (String, Int) = process_output(raw_execute(cwd, env, redirect, args: _*))
}
--- a/src/Pure/Thy/thy_output.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Mon Sep 20 12:03:11 2010 +0200
@@ -103,7 +103,7 @@
(case Symtab.lookup (! global_commands) name of
NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos)
| SOME f =>
- (Position.report (Markup.doc_antiq name) pos;
+ (Position.report pos (Markup.doc_antiq name);
(fn state => fn ctxt => f src state ctxt handle ERROR msg =>
cat_error msg ("The error(s) above occurred in document antiquotation: " ^
quote name ^ Position.str_of pos))))
--- a/src/Pure/Thy/thy_syntax.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Mon Sep 20 12:03:11 2010 +0200
@@ -84,7 +84,7 @@
Markup.enclose (token_markup tok) (Output.output (Token.unparse tok));
fun report_token tok =
- Position.report (token_markup tok) (Token.position_of tok);
+ Position.report (Token.position_of tok) (token_markup tok);
end;
@@ -152,7 +152,7 @@
Markup.enclose (kind_markup (span_kind span)) (implode (map present_token (span_content span)));
fun report_span span =
- Position.report (kind_markup (span_kind span)) (Position.encode_range (span_range span));
+ Position.report (Position.encode_range (span_range span)) (kind_markup (span_kind span));
end;
--- a/src/Pure/context_position.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/context_position.ML Mon Sep 20 12:03:11 2010 +0200
@@ -10,30 +10,25 @@
val set_visible: bool -> Proof.context -> Proof.context
val restore_visible: Proof.context -> Proof.context -> Proof.context
val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit
- val reported_text: Proof.context -> Markup.T -> Position.T -> string -> string
- val report_text: Proof.context -> Markup.T -> Position.T -> string -> unit
- val report: Proof.context -> Markup.T -> Position.T -> unit
+ val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
+ val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
+ val report: Proof.context -> Position.T -> Markup.T -> unit
end;
structure Context_Position: CONTEXT_POSITION =
struct
-structure Data = Proof_Data
-(
- type T = bool;
- fun init _ = true;
-);
-
-val is_visible = Data.get;
-val set_visible = Data.put;
+val visible = Config.bool (Config.declare "Context_Position.visible" (K (Config.Bool true)));
+fun is_visible ctxt = Config.get ctxt visible;
+val set_visible = Config.put visible;
val restore_visible = set_visible o is_visible;
fun if_visible ctxt f x = if is_visible ctxt then f x else ();
-fun reported_text ctxt markup pos txt =
- if is_visible ctxt then Position.reported_text markup pos txt else "";
+fun reported_text ctxt pos markup txt =
+ if is_visible ctxt then Position.reported_text pos markup txt else "";
-fun report_text ctxt markup pos txt = Output.report (reported_text ctxt markup pos txt);
-fun report ctxt markup pos = report_text ctxt markup pos "";
+fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt);
+fun report ctxt pos markup = report_text ctxt pos markup "";
end;
--- a/src/Pure/pure_thy.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/pure_thy.ML Mon Sep 20 12:03:11 2010 +0200
@@ -93,7 +93,7 @@
(case res of
NONE => error ("Unknown fact " ^ quote name ^ Position.str_of pos)
| SOME (static, ths) =>
- (Position.report ((if static then Markup.fact else Markup.dynamic_fact) name) pos;
+ (Position.report pos ((if static then Markup.fact else Markup.dynamic_fact) name);
Facts.select xthmref (map (Thm.transfer thy) ths)))
end;
@@ -188,7 +188,7 @@
let
val pos = Binding.pos_of b;
val name = Sign.full_name thy b;
- val _ = Position.report (Markup.fact_decl name) pos;
+ val _ = Position.report pos (Markup.fact_decl name);
fun app (x, (ths, atts)) = Library.foldl_map (Thm.theory_attributes atts) (x, ths);
val (thms, thy') = thy |> enter_thms
--- a/src/Pure/sign.ML Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Pure/sign.ML Mon Sep 20 12:03:11 2010 +0200
@@ -426,7 +426,7 @@
let
val pos = Binding.pos_of b;
val ([const as Const (c, _)], thy') = gen_add_consts (K I) [(b, T, mx)] thy;
- val _ = Position.report (Markup.const_decl c) pos;
+ val _ = Position.report pos (Markup.const_decl c);
in (const, thy') end;
end;
--- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css Mon Sep 20 12:03:11 2010 +0200
@@ -6,7 +6,6 @@
.tracing { background-color: #F0F8FF; }
.warning { background-color: #EEE8AA; }
.error { background-color: #FFC1C1; }
-.debug { background-color: #FFE4E1; }
.report { display: none; }
--- a/src/Tools/jEdit/dist-template/properties/jedit.props Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Mon Sep 20 12:03:11 2010 +0200
@@ -177,12 +177,12 @@
end.shortcut=
fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
firstTime=false
-foldPainter=Circle
home.shortcut=
insert-newline-indent.shortcut=
insert-newline.shortcut=ENTER
isabelle-output.dock-position=bottom
isabelle-raw-output.dock-position=bottom
+isabelle-session.dock-position=bottom
isabelle.activate.shortcut=CS+ENTER
line-end.shortcut=END
line-home.shortcut=HOME
--- a/src/Tools/jEdit/plugin/Isabelle.props Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props Mon Sep 20 12:03:11 2010 +0200
@@ -1,6 +1,6 @@
## Isabelle plugin properties
##
-##:encoding=ISO-8859-1:
+##:encoding=ISO-8859-1:wrap=soft:maxLineLen=100:
#identification
plugin.isabelle.jedit.Plugin.name=Isabelle
@@ -35,13 +35,15 @@
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.show-output isabelle.show-raw-output isabelle.show-protocol
+plugin.isabelle.jedit.Plugin.menu=isabelle.activate isabelle.session-panel isabelle.show-output isabelle.show-raw-output isabelle.show-protocol
isabelle.activate.label=Activate current buffer
+isabelle.session-panel.label=Prover session panel
isabelle.show-output.label=Show Output
isabelle.show-raw-output.label=Show Raw Output
isabelle.show-protocol.label=Show Protocol
#dockables
+isabelle-session.title=Session
isabelle-output.title=Output
isabelle-raw-output.title=Raw Output
isabelle-protocol.title=Protocol
--- a/src/Tools/jEdit/plugin/actions.xml Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Tools/jEdit/plugin/actions.xml Mon Sep 20 12:03:11 2010 +0200
@@ -10,6 +10,11 @@
return isabelle.jedit.Isabelle.is_active(view);
</IS_SELECTED>
</ACTION>
+ <ACTION NAME="isabelle.session-panel">
+ <CODE>
+ wm.addDockableWindow("isabelle-session");
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.show-output">
<CODE>
wm.addDockableWindow("isabelle-output");
--- a/src/Tools/jEdit/plugin/dockables.xml Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Tools/jEdit/plugin/dockables.xml Mon Sep 20 12:03:11 2010 +0200
@@ -2,6 +2,9 @@
<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
<DOCKABLES>
+ <DOCKABLE NAME="isabelle-session" MOVABLE="TRUE">
+ new isabelle.jedit.Session_Dockable(view, position);
+ </DOCKABLE>
<DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
new isabelle.jedit.Output_Dockable(view, position);
</DOCKABLE>
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Mon Sep 20 12:03:11 2010 +0200
@@ -54,10 +54,13 @@
if (snapshot.is_outdated) None
else
Isar_Document.command_status(state.status) match {
- case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
+ case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None
case Isar_Document.Unprocessed => Some(unfinished_color)
case Isar_Document.Failed => Some(error_color)
- case _ => None
+ case Isar_Document.Finished =>
+ if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
+ else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color)
+ else None
}
}
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Mon Sep 20 12:03:11 2010 +0200
@@ -7,36 +7,21 @@
package isabelle.jedit
-import javax.swing.{JComboBox, JSpinner}
+import javax.swing.JSpinner
import org.gjt.sp.jedit.AbstractOptionPane
class Isabelle_Options extends AbstractOptionPane("isabelle")
{
- private val logic_name = new JComboBox()
+ private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic"))
private val relative_font_size = new JSpinner()
private val tooltip_font_size = new JSpinner()
private val tooltip_dismiss_delay = new JSpinner()
- private class List_Item(val name: String, val descr: String) {
- def this(name: String) = this(name, name)
- override def toString = descr
- }
-
override def _init()
{
- val logic = Isabelle.Property("logic")
- addComponent(Isabelle.Property("logic.title"), {
- logic_name.addItem(new List_Item("", "default (" + Isabelle.default_logic() + ")"))
- for (name <- Isabelle.system.find_logics()) {
- val item = new List_Item(name)
- logic_name.addItem(item)
- if (name == logic)
- logic_name.setSelectedItem(item)
- }
- logic_name
- })
+ addComponent(Isabelle.Property("logic.title"), logic_selector.peer)
addComponent(Isabelle.Property("relative-font-size.title"), {
relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
@@ -57,7 +42,7 @@
override def _save()
{
Isabelle.Property("logic") =
- logic_name.getSelectedItem.asInstanceOf[List_Item].name
+ logic_selector.selection.item.name
Isabelle.Int_Property("relative-font-size") =
relative_font_size.getValue().asInstanceOf[Int]
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Sep 20 12:03:11 2010 +0200
@@ -26,13 +26,12 @@
val html_panel =
new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
- add(html_panel, BorderLayout.CENTER)
+ set_content(html_panel)
/* component state -- owned by Swing thread */
private var zoom_factor = 100
- private var show_debug = false
private var show_tracing = false
private var follow_caret = true
private var current_command: Option[Command] = None
@@ -68,8 +67,7 @@
val snapshot = doc_view.model.snapshot()
val filtered_results =
snapshot.state(cmd).results.iterator.map(_._2) filter {
- case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
- case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
+ case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing // FIXME not scalable
case _ => true
}
html_panel.render(filtered_results.toList)
@@ -122,13 +120,6 @@
private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
zoom.tooltip = "Zoom factor for basic font size"
- private val debug = new CheckBox("Debug") {
- reactions += { case ButtonClicked(_) => show_debug = this.selected; handle_update() }
- }
- debug.selected = show_debug
- debug.tooltip =
- "<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>"
-
private val tracing = new CheckBox("Tracing") {
reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
}
@@ -146,7 +137,7 @@
}
update.tooltip = "Update display according to the command at cursor position"
- val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update)
+ val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
add(controls.peer, BorderLayout.NORTH)
handle_update()
--- a/src/Tools/jEdit/src/jedit/plugin.scala Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Mon Sep 20 12:03:11 2010 +0200
@@ -11,9 +11,9 @@
import java.io.{FileInputStream, IOException}
import java.awt.Font
-import javax.swing.JTextArea
import scala.collection.mutable
+import scala.swing.ComboBox
import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
Buffer, EditPane, ServiceManager, View}
@@ -120,27 +120,6 @@
}
- /* settings */
-
- def default_logic(): String =
- {
- val logic = system.getenv("JEDIT_LOGIC")
- if (logic != "") logic
- else system.getenv_strict("ISABELLE_LOGIC")
- }
-
- def isabelle_args(): List[String] =
- {
- val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
- val logic = {
- val logic = Property("logic")
- if (logic != null && logic != "") logic
- else default_logic()
- }
- modes ++ List(logic)
- }
-
-
/* main jEdit components */
def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
@@ -170,6 +149,12 @@
private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
+ def docked_session(view: View): Option[Session_Dockable] =
+ wm(view).getDockableWindow("isabelle-session") match {
+ case dockable: Session_Dockable => Some(dockable)
+ case _ => None
+ }
+
def docked_output(view: View): Option[Output_Dockable] =
wm(view).getDockableWindow("isabelle-output") match {
case dockable: Output_Dockable => Some(dockable)
@@ -189,6 +174,45 @@
}
+ /* logic image */
+
+ def default_logic(): String =
+ {
+ val logic = system.getenv("JEDIT_LOGIC")
+ if (logic != "") logic
+ else system.getenv_strict("ISABELLE_LOGIC")
+ }
+
+ class Logic_Entry(val name: String, val description: String)
+ {
+ override def toString = description
+ }
+
+ def logic_selector(logic: String): ComboBox[Logic_Entry] =
+ {
+ val entries =
+ new Logic_Entry("", "default (" + default_logic() + ")") ::
+ system.find_logics().map(name => new Logic_Entry(name, name))
+ val component = new ComboBox(entries)
+ entries.find(_.name == logic) match {
+ case None =>
+ case Some(entry) => component.selection.item = entry
+ }
+ component
+ }
+
+ def isabelle_args(): List[String] =
+ {
+ val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
+ val logic = {
+ val logic = Property("logic")
+ if (logic != null && logic != "") logic
+ else default_logic()
+ }
+ modes ++ List(logic)
+ }
+
+
/* manage prover */ // FIXME async!?
private def prover_started(view: View): Boolean =
@@ -196,7 +220,8 @@
val timeout = Int_Property("startup-timeout") max 1000
session.started(timeout, Isabelle.isabelle_args()) match {
case Some(err) =>
- val text = new JTextArea(err); text.setEditable(false)
+ val text = new scala.swing.TextArea(err)
+ text.editable = false
Library.error_dialog(view, null, "Failed to start Isabelle process", text)
false
case None => true
--- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala Mon Sep 20 11:55:36 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/raw_output_dockable.scala Mon Sep 20 12:03:11 2010 +0200
@@ -19,6 +19,7 @@
extends Dockable(view: View, position: String)
{
private val text_area = new TextArea
+ text_area.editable = false
set_content(new ScrollPane(text_area))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/session_dockable.scala Mon Sep 20 12:03:11 2010 +0200
@@ -0,0 +1,37 @@
+/* Title: Tools/jEdit/src/jedit/session_dockable.scala
+ Author: Makarius
+
+Dockable window for prover session management.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.actors.Actor._
+import scala.swing.{TextArea, ScrollPane}
+
+import org.gjt.sp.jedit.View
+
+
+class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
+{
+ private val text_area = new TextArea("Isabelle session")
+ text_area.editable = false
+ set_content(new ScrollPane(text_area))
+
+
+ /* main actor */
+
+ private val main_actor = actor {
+ loop {
+ react {
+ case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def init() { }
+ override def exit() { }
+}