--- a/src/Pure/General/antiquote.ML Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/General/antiquote.ML Tue Sep 06 21:11:12 2011 +0200
@@ -12,7 +12,7 @@
Open of Position.T |
Close of Position.T
val is_text: 'a antiquote -> bool
- val report: ('a -> unit) -> 'a antiquote -> unit
+ val reports_of: ('a -> Position.report list) -> 'a antiquote list -> Position.report list
val check_nesting: 'a antiquote list -> unit
val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
@@ -35,14 +35,14 @@
| is_text _ = false;
-(* report *)
-
-fun report_antiq pos = Position.report pos Markup.antiq;
+(* reports *)
-fun report report_text (Text x) = report_text x
- | report _ (Antiq (_, (pos, _))) = report_antiq pos
- | report _ (Open pos) = report_antiq pos
- | report _ (Close pos) = report_antiq pos;
+fun reports_of text =
+ maps
+ (fn Text x => text x
+ | Antiq (_, (pos, _)) => [(pos, Markup.antiq)]
+ | Open pos => [(pos, Markup.antiq)]
+ | Close pos => [(pos, Markup.antiq)]);
(* check_nesting *)
@@ -97,7 +97,7 @@
fun read (syms, pos) =
(case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
- SOME xs => (List.app (report (K ())) xs; check_nesting xs; xs)
+ SOME xs => (Position.reports (reports_of (K []) xs); check_nesting xs; xs)
| NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
end;
--- a/src/Pure/General/position.ML Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/General/position.ML Tue Sep 06 21:11:12 2011 +0200
@@ -35,8 +35,9 @@
val reported_text: T -> Markup.T -> string -> string
val report_text: T -> Markup.T -> string -> unit
val report: T -> Markup.T -> unit
- type reports = (T * Markup.T) list
- val reports: reports Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
+ type report = T * Markup.T
+ val reports: report list -> unit
+ val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
val str_of: T -> string
type range = T * T
val no_range: range
@@ -154,10 +155,14 @@
fun report_text pos markup txt = Output.report (reported_text pos markup txt);
fun report pos markup = report_text pos markup "";
-type reports = (T * Markup.T) list;
+type report = T * Markup.T;
-fun reports _ [] _ _ = ()
- | reports (r: reports Unsynchronized.ref) ps markup x =
+val reports =
+ map (fn (pos, m) => if is_reported pos then Markup.markup_only (markup pos m) else "")
+ #> implode #> Output.report;
+
+fun store_reports _ [] _ _ = ()
+ | store_reports (r: report list Unsynchronized.ref) ps markup x =
let val ms = markup x
in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
--- a/src/Pure/Isar/outer_syntax.ML Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/Isar/outer_syntax.ML Tue Sep 06 21:11:12 2011 +0200
@@ -258,7 +258,7 @@
let
val commands = lookup_commands outer_syntax;
val range_pos = Position.set_range (Token.range toks);
- val _ = List.app Thy_Syntax.report_token toks;
+ val _ = Position.reports (maps Thy_Syntax.reports_of_token toks);
in
(case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
[tr] =>
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Sep 06 21:11:12 2011 +0200
@@ -34,31 +34,31 @@
fun report_parse_tree depth space =
let
- val report_text =
+ val reported_text =
(case Context.thread_data () of
- SOME (Context.Proof ctxt) => Context_Position.report_text ctxt
- | _ => Position.report_text);
+ SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
+ | _ => Position.reported_text);
- fun report_entity kind loc decl =
- report_text (position_of loc)
+ fun reported_entity kind loc decl =
+ reported_text (position_of loc)
(Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
- fun report loc (PolyML.PTtype types) =
- cons (fn () =>
- PolyML.NameSpace.displayTypeExpression (types, depth, space)
- |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
- |> report_text (position_of loc) Markup.ML_typing)
- | report loc (PolyML.PTdeclaredAt decl) =
- cons (fn () => report_entity Markup.ML_defN loc decl)
- | report loc (PolyML.PTopenedAt decl) =
- cons (fn () => report_entity Markup.ML_openN loc decl)
- | report loc (PolyML.PTstructureAt decl) =
- cons (fn () => report_entity Markup.ML_structN loc decl)
- | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
- | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
- | report _ _ = I
- and report_tree (loc, props) = fold (report loc) props;
- in fn tree => List.app (fn e => e ()) (report_tree tree []) end;
+ fun reported loc (PolyML.PTtype types) =
+ cons
+ (PolyML.NameSpace.displayTypeExpression (types, depth, space)
+ |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
+ |> reported_text (position_of loc) Markup.ML_typing)
+ | reported loc (PolyML.PTdeclaredAt decl) =
+ cons (reported_entity Markup.ML_defN loc decl)
+ | reported loc (PolyML.PTopenedAt decl) =
+ cons (reported_entity Markup.ML_openN loc decl)
+ | reported loc (PolyML.PTstructureAt decl) =
+ cons (reported_entity Markup.ML_structN loc decl)
+ | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
+ | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
+ | reported _ _ = I
+ and reported_tree (loc, props) = fold (reported loc) props;
+ in fn tree => Output.report (implode (reported_tree tree [])) end;
(* eval ML source tokens *)
--- a/src/Pure/ML/ml_lex.ML Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/ML/ml_lex.ML Tue Sep 06 21:11:12 2011 +0200
@@ -20,7 +20,6 @@
val content_of: token -> string
val check_content_of: token -> string
val flatten: token list -> string
- val report_token: token -> unit
val keywords: string list
val source: (Symbol.symbol, 'a) Source.source ->
(token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
@@ -126,7 +125,7 @@
in
-fun report_token (Token ((pos, _), (kind, x))) = Position.report pos (token_markup kind x);
+fun report_of_token (Token ((pos, _), (kind, x))) = (pos, token_markup kind x);
end;
@@ -293,7 +292,7 @@
|> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
(SOME (false, fn msg => recover msg >> map Antiquote.Text))
|> Source.exhaust
- |> tap (List.app (Antiquote.report report_token))
+ |> tap (Position.reports o Antiquote.reports_of (single o report_of_token))
|> tap Antiquote.check_nesting
|> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
handle ERROR msg =>
--- a/src/Pure/Syntax/lexicon.ML Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/Syntax/lexicon.ML Tue Sep 06 21:11:12 2011 +0200
@@ -44,7 +44,7 @@
val tvarT: typ
val terminals: string list
val is_terminal: string -> bool
- val report_token: Proof.context -> token -> unit
+ val report_of_token: token -> Position.report
val reported_token_range: Proof.context -> token -> string
val matching_tokens: token * token -> bool
val valued_token: token -> bool
@@ -203,11 +203,11 @@
| Comment => Markup.inner_comment
| EOF => Markup.empty;
-fun report_token ctxt (Token (kind, s, (pos, _))) =
+fun report_of_token (Token (kind, s, (pos, _))) =
let val markup =
if kind = Literal andalso not (is_ascii_identifier s) then Markup.delimiter
else token_kind_markup kind
- in Context_Position.report ctxt pos markup end;
+ in (pos, markup) end;
fun reported_token_range ctxt tok =
if is_proper tok
--- a/src/Pure/Syntax/syntax_phases.ML Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/Syntax/syntax_phases.ML Tue Sep 06 21:11:12 2011 +0200
@@ -10,7 +10,7 @@
val term_sorts: term -> (indexname * sort) list
val typ_of_term: (indexname -> sort) -> term -> typ
val decode_term: Proof.context ->
- Position.reports * term Exn.result -> Position.reports * term Exn.result
+ Position.report list * term Exn.result -> Position.report list * term Exn.result
val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
val term_of_typ: Proof.context -> typ -> term
end
@@ -126,8 +126,8 @@
fun parsetree_to_ast ctxt constrain_pos trf parsetree =
let
- val reports = Unsynchronized.ref ([]: Position.reports);
- fun report pos = Position.reports reports [pos];
+ val reports = Unsynchronized.ref ([]: Position.report list);
+ fun report pos = Position.store_reports reports [pos];
fun trans a args =
(case trf a of
@@ -196,7 +196,7 @@
(* decode_term -- transform parse tree into raw term *)
-fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
+fun decode_term _ (result as (_: Position.report list, Exn.Exn _)) = result
| decode_term ctxt (reports0, Exn.Res tm) =
let
fun get_const a =
@@ -207,7 +207,7 @@
val decodeT = typ_of_term (Proof_Context.get_sort ctxt (term_sorts tm));
val reports = Unsynchronized.ref reports0;
- fun report ps = Position.reports reports ps;
+ fun report ps = Position.store_reports reports ps;
fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
(case Term_Position.decode_position typ of
@@ -262,12 +262,10 @@
fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
-fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
-
fun report_result ctxt pos results =
(case (proper_results results, failed_results results) of
- ([], (reports, exn) :: _) => (report ctxt reports; reraise exn)
- | ([(reports, x)], _) => (report ctxt reports; x)
+ ([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn)
+ | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x)
| _ => error (ambiguity_msg pos));
@@ -279,7 +277,7 @@
val ast_tr = Syntax.parse_ast_translation syn;
val toks = Syntax.tokenize syn raw syms;
- val _ = List.app (Lexicon.report_token ctxt) toks;
+ val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
val pts = Syntax.parse ctxt syn root (filter Lexicon.is_proper toks)
handle ERROR msg =>
--- a/src/Pure/System/isabelle_process.ML Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/System/isabelle_process.ML Tue Sep 06 21:11:12 2011 +0200
@@ -66,27 +66,29 @@
fun chunk s = [string_of_int (size s), "\n", s];
-fun message mbox ch raw_props body =
+fun message do_flush mbox ch raw_props body =
let
val robust_props = map (pairself YXML.embed_controls) raw_props;
val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
- in Mailbox.send mbox (chunk header @ chunk body) end;
+ in Mailbox.send mbox (chunk header @ chunk body, do_flush) end;
fun standard_message mbox opt_serial ch body =
if body = "" then ()
else
- message mbox ch
+ message false mbox ch
((case opt_serial of SOME i => cons (Markup.serialN, string_of_int i) | _ => I)
(Position.properties_of (Position.thread_data ()))) body;
fun message_output mbox out_stream =
let
+ fun flush () = ignore (try TextIO.flushOut out_stream);
fun loop receive =
(case receive mbox of
- SOME msg =>
+ SOME (msg, do_flush) =>
(List.app (fn s => TextIO.output (out_stream, s)) msg;
+ if do_flush then flush () else ();
loop (Mailbox.receive_timeout (seconds 0.02)))
- | NONE => (try TextIO.flushOut out_stream; loop (SOME o Mailbox.receive)));
+ | NONE => (flush (); loop (SOME o Mailbox.receive)));
in fn () => loop (SOME o Mailbox.receive) end;
in
@@ -100,7 +102,7 @@
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
- val mbox = Mailbox.create () : string list Mailbox.T;
+ val mbox = Mailbox.create () : (string list * bool) Mailbox.T;
val _ = Simple_Thread.fork false (message_output mbox out_stream);
in
Output.Private_Hooks.status_fn := standard_message mbox NONE "B";
@@ -109,10 +111,10 @@
Output.Private_Hooks.tracing_fn := (fn s => standard_message mbox (SOME (serial ())) "E" s);
Output.Private_Hooks.warning_fn := (fn s => standard_message mbox (SOME (serial ())) "F" s);
Output.Private_Hooks.error_fn := (fn (i, s) => standard_message mbox (SOME i) "G" s);
- Output.Private_Hooks.raw_message_fn := message mbox "H";
+ Output.Private_Hooks.raw_message_fn := message true mbox "H";
Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
Output.Private_Hooks.prompt_fn := ignore;
- message mbox "A" [] (Session.welcome ());
+ message true mbox "A" [] (Session.welcome ());
in_stream
end;
--- a/src/Pure/System/isabelle_process.scala Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/System/isabelle_process.scala Tue Sep 06 21:11:12 2011 +0200
@@ -33,7 +33,7 @@
('H' : Int) -> Markup.RAW)
}
- abstract class Message
+ sealed abstract class Message
class Input(name: String, args: List[String]) extends Message
{
@@ -75,22 +75,21 @@
}
-class Isabelle_Process(timeout: Time, receiver: Actor, args: String*)
+class Isabelle_Process(timeout: Time, receiver: Isabelle_Process.Message => Unit, args: String*)
{
import Isabelle_Process._
/* demo constructor */
- def this(args: String*) =
- this(Time.seconds(10), actor { loop { react { case res => Console.println(res) } } }, args: _*)
+ def this(args: String*) = this(Time.seconds(10), Console.println(_), args: _*)
/* results */
private def system_result(text: String)
{
- receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
+ receiver(new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))))
}
private val xml_cache = new XML.Cache()
@@ -99,10 +98,10 @@
{
if (kind == Markup.INIT) rm_fifos()
if (kind == Markup.RAW)
- receiver ! new Result(XML.Elem(Markup(kind, props), body))
+ receiver(new Result(XML.Elem(Markup(kind, props), body)))
else {
val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
- receiver ! new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem])
+ receiver(new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
}
}
@@ -399,7 +398,7 @@
def input(name: String, args: String*): Unit =
{
- receiver ! new Input(name, args.toList)
+ receiver(new Input(name, args.toList))
input_bytes(name, args.map(Standard_System.string_bytes): _*)
}
--- a/src/Pure/System/session.scala Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/System/session.scala Tue Sep 06 21:11:12 2011 +0200
@@ -7,8 +7,11 @@
package isabelle
+
import java.lang.System
+import java.util.{Timer, TimerTask}
+import scala.collection.mutable
import scala.actors.TIMEOUT
import scala.actors.Actor._
@@ -37,6 +40,7 @@
{
/* real time parameters */ // FIXME properties or settings (!?)
+ val message_delay = Time.seconds(0.01) // prover messages
val input_delay = Time.seconds(0.3) // user input (e.g. text edits, cursor movement)
val output_delay = Time.seconds(0.1) // prover output (markup, common messages)
val update_delay = Time.seconds(0.5) // GUI layout updates
@@ -52,7 +56,9 @@
val assignments = new Event_Bus[Session.Assignment.type]
val commands_changed = new Event_Bus[Session.Commands_Changed]
val phase_changed = new Event_Bus[Session.Phase]
- val raw_messages = new Event_Bus[Isabelle_Process.Message]
+ val syslog_messages = new Event_Bus[Isabelle_Process.Result]
+ val raw_output_messages = new Event_Bus[Isabelle_Process.Result]
+ val raw_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck
@@ -141,15 +147,45 @@
doc_edits: List[Document.Edit_Command],
previous: Document.Version,
version: Document.Version)
+ private case class Messages(msgs: List[Isabelle_Process.Message])
private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
{
val this_actor = self
- var prover: Option[Isabelle_Process with Isar_Document] = None
var prune_next = System.currentTimeMillis() + prune_delay.ms
+ /* buffered prover messages */
+
+ object receiver
+ {
+ private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
+
+ def flush(): Unit = synchronized {
+ if (!buffer.isEmpty) {
+ val msgs = buffer.toList
+ this_actor ! Messages(msgs)
+ buffer = new mutable.ListBuffer[Isabelle_Process.Message]
+ }
+ }
+ def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
+ buffer += msg
+ msg match {
+ case result: Isabelle_Process.Result if result.is_raw => flush()
+ case _ =>
+ }
+ }
+
+ private val timer = new Timer("session_actor.receiver", true)
+ timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
+
+ def cancel() { timer.cancel() }
+ }
+
+ var prover: Option[Isabelle_Process with Isar_Document] = None
+
+
/* delayed command changes */
object commands_changed_delay
@@ -371,7 +407,8 @@
case Start(timeout, args) if prover.isEmpty =>
if (phase == Session.Inactive || phase == Session.Failed) {
phase = Session.Startup
- prover = Some(new Isabelle_Process(timeout, this_actor, args:_*) with Isar_Document)
+ prover =
+ Some(new Isabelle_Process(timeout, receiver.invoke _, args:_*) with Isar_Document)
}
case Stop =>
@@ -383,6 +420,7 @@
phase = Session.Inactive
}
finished = true
+ receiver.cancel()
reply(())
case Interrupt if prover.isDefined =>
@@ -408,12 +446,17 @@
case change: Change_Node if prover.isDefined =>
handle_change(change)
- case input: Isabelle_Process.Input =>
- raw_messages.event(input)
+ case Messages(msgs) =>
+ msgs foreach {
+ case input: Isabelle_Process.Input =>
+ raw_messages.event(input)
- case result: Isabelle_Process.Result =>
- handle_result(result)
- raw_messages.event(result)
+ case result: Isabelle_Process.Result =>
+ handle_result(result)
+ if (result.is_syslog) syslog_messages.event(result)
+ if (result.is_stdout) raw_output_messages.event(result)
+ raw_messages.event(result)
+ }
case bad => System.err.println("session_actor: ignoring bad message " + bad)
}
--- a/src/Pure/Thy/thy_syntax.ML Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/Thy/thy_syntax.ML Tue Sep 06 21:11:12 2011 +0200
@@ -11,7 +11,7 @@
Source.source) Source.source) Source.source) Source.source
val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
val present_token: Token.T -> Output.output
- val report_token: Token.T -> unit
+ val reports_of_token: Token.T -> Position.report list
datatype span_kind = Command of string | Ignored | Malformed
type span
val span_kind: span -> span_kind
@@ -74,17 +74,17 @@
else I;
in props (token_kind_markup kind) end;
-fun report_symbol (sym, pos) =
- if Symbol.is_malformed sym then Position.report pos Markup.malformed else ();
+fun reports_of_symbol (sym, pos) =
+ if Symbol.is_malformed sym then [(pos, Markup.malformed)] else [];
in
fun present_token tok =
Markup.enclose (token_markup tok) (Output.output (Token.unparse tok));
-fun report_token tok =
- (Position.report (Token.position_of tok) (token_markup tok);
- List.app report_symbol (Symbol_Pos.explode (Token.source_position_of tok)));
+fun reports_of_token tok =
+ (Token.position_of tok, token_markup tok) ::
+ maps reports_of_symbol (Symbol_Pos.explode (Token.source_position_of tok));
end;
--- a/src/Pure/context_position.ML Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Pure/context_position.ML Tue Sep 06 21:11:12 2011 +0200
@@ -14,6 +14,7 @@
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
+ val reports: Proof.context -> Position.report list -> unit
end;
structure Context_Position: CONTEXT_POSITION =
@@ -35,4 +36,6 @@
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 "";
+fun reports ctxt reps = if is_visible ctxt then Position.reports reps else ();
+
end;
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Tue Sep 06 21:11:12 2011 +0200
@@ -29,8 +29,6 @@
private val main_actor = actor {
loop {
react {
- case input: Isabelle_Process.Input =>
-
case result: Isabelle_Process.Result =>
if (result.is_stdout)
Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
@@ -40,6 +38,6 @@
}
}
- override def init() { Isabelle.session.raw_messages += main_actor }
- override def exit() { Isabelle.session.raw_messages -= main_actor }
+ override def init() { Isabelle.session.raw_output_messages += main_actor }
+ override def exit() { Isabelle.session.raw_output_messages -= main_actor }
}
--- a/src/Tools/jEdit/src/session_dockable.scala Tue Sep 06 10:30:33 2011 -0700
+++ b/src/Tools/jEdit/src/session_dockable.scala Tue Sep 06 21:11:12 2011 +0200
@@ -105,8 +105,6 @@
private val main_actor = actor {
loop {
react {
- case input: Isabelle_Process.Input =>
-
case result: Isabelle_Process.Result =>
if (result.is_syslog)
Swing_Thread.now {
@@ -127,13 +125,13 @@
}
override def init() {
- Isabelle.session.raw_messages += main_actor
+ Isabelle.session.syslog_messages += main_actor
Isabelle.session.phase_changed += main_actor
Isabelle.session.commands_changed += main_actor
}
override def exit() {
- Isabelle.session.raw_messages -= main_actor
+ Isabelle.session.syslog_messages -= main_actor
Isabelle.session.phase_changed -= main_actor
Isabelle.session.commands_changed -= main_actor
}