--- a/src/HOL/MicroJava/J/JBasis.thy Fri Nov 25 19:07:26 2011 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy Fri Nov 25 22:21:37 2011 +0100
@@ -14,59 +14,37 @@
section "unique"
definition unique :: "('a \<times> 'b) list => bool" where
- "unique == distinct \<circ> map fst"
+ "unique == distinct \<circ> map fst"
-lemma fst_in_set_lemma [rule_format (no_asm)]:
- "(x, y) : set xys --> x : fst ` set xys"
-apply (induct_tac "xys")
-apply auto
-done
+lemma fst_in_set_lemma: "(x, y) : set xys ==> x : fst ` set xys"
+ by (induct xys) auto
lemma unique_Nil [simp]: "unique []"
-apply (unfold unique_def)
-apply (simp (no_asm))
-done
+ by (simp add: unique_def)
lemma unique_Cons [simp]: "unique ((x,y)#l) = (unique l & (!y. (x,y) ~: set l))"
-apply (unfold unique_def)
-apply (auto dest: fst_in_set_lemma)
-done
+ by (auto simp: unique_def dest: fst_in_set_lemma)
-lemma unique_append [rule_format (no_asm)]: "unique l' ==> unique l -->
- (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')"
-apply (induct_tac "l")
-apply (auto dest: fst_in_set_lemma)
-done
+lemma unique_append: "unique l' ==> unique l ==>
+ (!(x,y):set l. !(x',y'):set l'. x' ~= x) ==> unique (l @ l')"
+ by (induct l) (auto dest: fst_in_set_lemma)
-lemma unique_map_inj [rule_format (no_asm)]:
- "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)"
-apply (induct_tac "l")
-apply (auto dest: fst_in_set_lemma simp add: inj_eq)
-done
+lemma unique_map_inj: "unique l ==> inj f ==> unique (map (%(k,x). (f k, g k x)) l)"
+ by (induct l) (auto dest: fst_in_set_lemma simp add: inj_eq)
+
section "More about Maps"
-lemma map_of_SomeI [rule_format (no_asm)]:
- "unique l --> (k, x) : set l --> map_of l k = Some x"
-apply (induct_tac "l")
-apply auto
-done
+lemma map_of_SomeI: "unique l ==> (k, x) : set l ==> map_of l k = Some x"
+ by (induct l) auto
-lemma Ball_set_table':
- "(\<forall>(x,y)\<in>set l. P x y) --> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)"
-apply(induct_tac "l")
-apply(simp_all (no_asm))
-apply safe
-apply auto
-done
-lemmas Ball_set_table = Ball_set_table' [THEN mp];
+lemma Ball_set_table: "(\<forall>(x,y)\<in>set l. P x y) ==> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)"
+ by (induct l) auto
-lemma table_of_remap_SomeD [rule_format (no_asm)]:
-"map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) -->
- map_of t (k, k') = Some x"
-apply (induct_tac "t")
-apply auto
-done
+lemma table_of_remap_SomeD:
+ "map_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) ==>
+ map_of t (k, k') = Some x"
+ by (atomize (full), induct t) auto
end
--- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Fri Nov 25 19:07:26 2011 +0100
+++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy Fri Nov 25 22:21:37 2011 +0100
@@ -114,8 +114,8 @@
(-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
proof -
assume "a \<in> zOdd"
- from QRLemma4 [OF this, symmetric] have
- "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" .
+ from QRLemma4 [OF this] have
+ "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" ..
moreover have "0 \<le> int(card E)"
by auto
moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"
--- a/src/HOL/Predicate.thy Fri Nov 25 19:07:26 2011 +0100
+++ b/src/HOL/Predicate.thy Fri Nov 25 22:21:37 2011 +0100
@@ -145,16 +145,16 @@
subsubsection {* Binary union *}
-lemma sup1I1 [elim?]: "A x \<Longrightarrow> (A \<squnion> B) x"
+lemma sup1I1 [intro?]: "A x \<Longrightarrow> (A \<squnion> B) x"
by (simp add: sup_fun_def)
-lemma sup2I1 [elim?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
+lemma sup2I1 [intro?]: "A x y \<Longrightarrow> (A \<squnion> B) x y"
by (simp add: sup_fun_def)
-lemma sup1I2 [elim?]: "B x \<Longrightarrow> (A \<squnion> B) x"
+lemma sup1I2 [intro?]: "B x \<Longrightarrow> (A \<squnion> B) x"
by (simp add: sup_fun_def)
-lemma sup2I2 [elim?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
+lemma sup2I2 [intro?]: "B x y \<Longrightarrow> (A \<squnion> B) x y"
by (simp add: sup_fun_def)
lemma sup1E [elim!]: "(A \<squnion> B) x \<Longrightarrow> (A x \<Longrightarrow> P) \<Longrightarrow> (B x \<Longrightarrow> P) \<Longrightarrow> P"
--- a/src/Pure/General/markup.scala Fri Nov 25 19:07:26 2011 +0100
+++ b/src/Pure/General/markup.scala Fri Nov 25 22:21:37 2011 +0100
@@ -257,6 +257,7 @@
val RAW = "raw"
val SYSTEM = "system"
val STDOUT = "stdout"
+ val STDERR = "stderr"
val EXIT = "exit"
val LEGACY = "legacy"
--- a/src/Pure/PIDE/text.scala Fri Nov 25 19:07:26 2011 +0100
+++ b/src/Pure/PIDE/text.scala Fri Nov 25 22:21:37 2011 +0100
@@ -101,6 +101,13 @@
def range: Range =
if (is_empty) Range(0)
else Range(ranges.head.start, ranges.last.stop)
+
+ override def hashCode: Int = ranges.hashCode
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Perspective => ranges == other.ranges
+ case _ => false
+ }
override def toString = ranges.toString
}
--- a/src/Pure/Syntax/parser.ML Fri Nov 25 19:07:26 2011 +0100
+++ b/src/Pure/Syntax/parser.ML Fri Nov 25 22:21:37 2011 +0100
@@ -9,7 +9,7 @@
type gram
val empty_gram: gram
val extend_gram: Syntax_Ext.xprod list -> gram -> gram
- val merge_gram: gram * gram -> gram
+ val make_gram: Syntax_Ext.xprod list -> gram
val pretty_gram: gram -> Pretty.T list
datatype parsetree =
Node of string * parsetree list |
@@ -526,105 +526,7 @@
prods = Array.vector prods'}
end;
-
-(*Merge two grammars*)
-fun merge_gram (gram_a, gram_b) =
- let
- (*find out which grammar is bigger*)
- val
- (Gram {nt_count = nt_count1, prod_count = prod_count1, tags = tags1,
- chains = chains1, lambdas = lambdas1, prods = prods1},
- Gram {nt_count = nt_count2, prod_count = prod_count2, tags = tags2,
- chains = chains2, lambdas = lambdas2, prods = prods2}) =
- let
- val Gram {prod_count = count_a, ...} = gram_a;
- val Gram {prod_count = count_b, ...} = gram_b;
- in
- if count_a > count_b
- then (gram_a, gram_b)
- else (gram_b, gram_a)
- end;
-
- (*get existing tag from grammar1 or create a new one*)
- fun get_tag nt_count tags nt =
- (case Symtab.lookup tags nt of
- SOME tag => (nt_count, tags, tag)
- | NONE => (nt_count + 1, Symtab.update_new (nt, nt_count) tags, nt_count));
-
- val ((nt_count1', tags1'), tag_table) =
- let
- val table = Array.array (nt_count2, ~1);
-
- fun the_nt tag =
- the (Symtab.get_first (fn (n, t) => if t = tag then SOME n else NONE) tags2);
- fun store_tag nt_count tags ~1 = (nt_count, tags)
- | store_tag nt_count tags tag =
- let
- val (nt_count', tags', tag') = get_tag nt_count tags (the_nt tag);
- val _ = Array.update (table, tag, tag');
- in store_tag nt_count' tags' (tag - 1) end;
- in (store_tag nt_count1 tags1 (nt_count2 - 1), table) end;
-
- (*convert grammar2 tag to grammar1 tag*)
- fun convert_tag tag = Array.sub (tag_table, tag);
-
- (*convert chain list to raw productions*)
- fun mk_chain_prods [] result = result
- | mk_chain_prods ((to, froms) :: cs) result =
- let
- val to_tag = convert_tag to;
-
- fun make [] result = result
- | make (from :: froms) result = make froms
- ((to_tag, ([Nonterminal (convert_tag from, ~1)], "", ~1)) :: result);
- in mk_chain_prods cs (make froms [] @ result) end;
-
- val chain_prods = mk_chain_prods chains2 [];
-
- (*convert prods2 array to productions*)
- fun process_nt ~1 result = result
- | process_nt nt result =
- let
- val nt_prods = fold (union (op =) o snd) (snd (Vector.sub (prods2, nt))) [];
- val lhs_tag = convert_tag nt;
-
- (*convert tags in rhs*)
- fun process_rhs [] result = result
- | process_rhs (Terminal tk :: rhs) result =
- process_rhs rhs (result @ [Terminal tk])
- | process_rhs (Nonterminal (nt, prec) :: rhs) result =
- process_rhs rhs (result @ [Nonterminal (convert_tag nt, prec)]);
-
- (*convert tags in productions*)
- fun process_prods [] result = result
- | process_prods ((rhs, id, prec) :: ps) result =
- process_prods ps ((lhs_tag, (process_rhs rhs [], id, prec)) :: result);
- in process_nt (nt - 1) (process_prods nt_prods [] @ result) end;
-
- val raw_prods = chain_prods @ process_nt (nt_count2 - 1) [];
-
- val prods1' =
- let
- fun get_prod i =
- if i < nt_count1 then Vector.sub (prods1, i)
- else (([], []), []);
- in Array.tabulate (nt_count1', get_prod) end;
-
- val fromto_chains = inverse_chains chains1 [];
-
- val (fromto_chains', lambdas', SOME prod_count1') =
- add_prods prods1' fromto_chains lambdas1 (SOME prod_count1) raw_prods;
-
- val chains' = inverse_chains fromto_chains' [];
- in
- Gram
- {nt_count = nt_count1',
- prod_count = prod_count1',
- tags = tags1',
- chains = chains',
- lambdas = lambdas',
- prods = Array.vector prods1'}
- end;
+fun make_gram xprods = extend_gram xprods empty_gram;
--- a/src/Pure/Syntax/syntax.ML Fri Nov 25 19:07:26 2011 +0100
+++ b/src/Pure/Syntax/syntax.ML Fri Nov 25 22:21:37 2011 +0100
@@ -74,7 +74,7 @@
val string_of_sort_global: theory -> sort -> string
type syntax
val eq_syntax: syntax * syntax -> bool
- val join_syntax: syntax -> unit
+ val force_syntax: syntax -> unit
val lookup_const: syntax -> string -> string option
val is_keyword: syntax -> string -> bool
val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
@@ -92,7 +92,7 @@
val mode_default: mode
val mode_input: mode
val empty_syntax: syntax
- val merge_syntaxes: syntax -> syntax -> syntax
+ val merge_syntax: syntax * syntax -> syntax
val token_markers: string list
val basic_nonterms: string list
val print_gram: syntax -> unit
@@ -379,16 +379,11 @@
(** datatype syntax **)
-fun future_gram deps e =
- singleton
- (Future.cond_forks {name = "Syntax.gram", group = NONE,
- deps = map Future.task_of deps, pri = 0, interrupts = true}) e;
-
datatype syntax =
Syntax of {
input: Syntax_Ext.xprod list,
lexicon: Scan.lexicon,
- gram: Parser.gram future,
+ gram: Parser.gram lazy,
consts: string Symtab.table,
prmodes: string list,
parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
@@ -401,12 +396,12 @@
fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
-fun join_syntax (Syntax ({gram, ...}, _)) = ignore (Future.join gram);
+fun force_syntax (Syntax ({gram, ...}, _)) = ignore (Lazy.force gram);
fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts;
fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
-fun parse ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt (Future.join gram);
+fun parse ctxt (Syntax ({gram, ...}, _)) = Parser.parse ctxt (Lazy.force gram);
fun parse_ast_translation (Syntax ({parse_ast_trtab, ...}, _)) = lookup_tr parse_ast_trtab;
fun parse_translation (Syntax ({parse_trtab, ...}, _)) = lookup_tr parse_trtab;
@@ -427,7 +422,7 @@
val empty_syntax = Syntax
({input = [],
lexicon = Scan.empty_lexicon,
- gram = Future.value Parser.empty_gram,
+ gram = Lazy.value Parser.empty_gram,
consts = Symtab.empty,
prmodes = [],
parse_ast_trtab = Symtab.empty,
@@ -460,7 +455,7 @@
Syntax
({input = new_xprods @ input,
lexicon = fold Scan.extend_lexicon (Syntax_Ext.delims_of new_xprods) lexicon,
- gram = Future.value (Parser.extend_gram new_xprods (Future.join gram)),
+ gram = Lazy.value (Parser.extend_gram new_xprods (Lazy.force gram)),
consts = fold update_const consts2 consts1,
prmodes = insert (op =) mode prmodes,
parse_ast_trtab =
@@ -489,7 +484,7 @@
Syntax
({input = input',
lexicon = if changed then Scan.make_lexicon (Syntax_Ext.delims_of input') else lexicon,
- gram = if changed then Future.value (Parser.extend_gram input' Parser.empty_gram) else gram,
+ gram = if changed then Lazy.value (Parser.make_gram input') else gram,
consts = consts,
prmodes = prmodes,
parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab,
@@ -502,9 +497,9 @@
end;
-(* merge_syntaxes *)
+(* merge_syntax *)
-fun merge_syntaxes (Syntax (tabs1, _)) (Syntax (tabs2, _)) =
+fun merge_syntax (Syntax (tabs1, _), Syntax (tabs2, _)) =
let
val {input = input1, lexicon = lexicon1, gram = gram1, consts = consts1,
prmodes = prmodes1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
@@ -515,12 +510,22 @@
prmodes = prmodes2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
parse_trtab = parse_trtab2, print_trtab = print_trtab2, print_ruletab = print_ruletab2,
print_ast_trtab = print_ast_trtab2, prtabs = prtabs2} = tabs2;
+
+ val (input', gram') =
+ (case subtract (op =) input1 input2 of
+ [] => (input1, gram1)
+ | new_xprods2 =>
+ if subset (op =) (input1, input2) then (input2, gram2)
+ else
+ let
+ val input' = new_xprods2 @ input1;
+ val gram' = Lazy.lazy (fn () => Parser.make_gram input');
+ in (input', gram') end);
in
Syntax
- ({input = Library.merge (op =) (input1, input2),
+ ({input = input',
lexicon = Scan.merge_lexicons (lexicon1, lexicon2),
- gram = future_gram [gram1, gram2] (fn () =>
- Parser.merge_gram (Future.join gram1, Future.join gram2)),
+ gram = gram',
consts = Symtab.merge (K true) (consts1, consts2),
prmodes = Library.merge (op =) (prmodes1, prmodes2),
parse_ast_trtab =
@@ -560,7 +565,7 @@
val prmodes' = sort_strings (filter_out (fn s => s = "") prmodes);
in
[pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
- Pretty.big_list "prods:" (Parser.pretty_gram (Future.join gram)),
+ Pretty.big_list "prods:" (Parser.pretty_gram (Lazy.force gram)),
pretty_strs_qs "print modes:" prmodes']
end;
@@ -596,7 +601,7 @@
(* reconstructing infixes -- educated guessing *)
fun guess_infix (Syntax ({gram, ...}, _)) c =
- (case Parser.guess_infix_lr (Future.join gram) c of
+ (case Parser.guess_infix_lr (Lazy.force gram) c of
SOME (s, l, r, j) => SOME
(if l then Mixfix.Infixl (s, j)
else if r then Mixfix.Infixr (s, j)
--- a/src/Pure/System/event_bus.scala Fri Nov 25 19:07:26 2011 +0100
+++ b/src/Pure/System/event_bus.scala Fri Nov 25 22:21:37 2011 +0100
@@ -32,29 +32,4 @@
/* event invocation */
def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
-
-
- /* await global condition -- triggered via bus events */
-
- def await(cond: => Boolean)
- {
- case object Wait
- val a = new Actor {
- def act {
- if (cond) react { case Wait => reply(()); exit(Wait) }
- else {
- loop {
- react {
- case trigger if trigger != Wait =>
- if (cond) { react { case Wait => reply(()); exit(Wait) } }
- }
- }
- }
- }
- }
- this += a
- a.start
- a !? Wait
- this -= a
- }
}
--- a/src/Pure/System/isabelle_process.scala Fri Nov 25 19:07:26 2011 +0100
+++ b/src/Pure/System/isabelle_process.scala Fri Nov 25 22:21:37 2011 +0100
@@ -52,12 +52,13 @@
def is_init = kind == Markup.INIT
def is_exit = kind == Markup.EXIT
def is_stdout = kind == Markup.STDOUT
+ def is_stderr = kind == Markup.STDERR
def is_system = kind == Markup.SYSTEM
def is_status = kind == Markup.STATUS
def is_report = kind == Markup.REPORT
def is_raw = kind == Markup.RAW
def is_ready = Isar_Document.is_ready(message)
- def is_syslog = is_init || is_exit || is_system || is_ready
+ def is_syslog = is_init || is_exit || is_system || is_ready || is_stderr
override def toString: String =
{
@@ -136,7 +137,7 @@
val cmdline =
Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
(system_channel.isabelle_args ::: args)
- new Isabelle_System.Managed_Process(true, cmdline: _*)
+ new Isabelle_System.Managed_Process(false, cmdline: _*)
}
catch { case e: IOException => system_channel.accepted(); throw(e) }
@@ -181,13 +182,15 @@
val (command_stream, message_stream) = system_channel.rendezvous()
standard_input = stdin_actor()
- val stdout = stdout_actor()
+ val stdout = raw_output_actor(false)
+ val stderr = raw_output_actor(true)
command_input = input_actor(command_stream)
val message = message_actor(message_stream)
val rc = process_result.join
system_result("process terminated")
- for ((thread, _) <- List(standard_input, stdout, command_input, message)) thread.join
+ for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
+ thread.join
system_result("process_manager terminated")
put_result(Markup.EXIT, "Return code: " + rc.toString)
}
@@ -238,11 +241,14 @@
}
- /* raw stdout */
+ /* raw output */
- private def stdout_actor(): (Thread, Actor) =
+ private def raw_output_actor(err: Boolean): (Thread, Actor) =
{
- val name = "standard_output"
+ val (name, reader, markup) =
+ if (err) ("standard_error", process.stderr, Markup.STDERR)
+ else ("standard_output", process.stdout, Markup.STDOUT)
+
Simple_Thread.actor(name) {
var result = new StringBuilder(100)
@@ -252,17 +258,17 @@
//{{{
var c = -1
var done = false
- while (!done && (result.length == 0 || process.stdout.ready)) {
- c = process.stdout.read
+ while (!done && (result.length == 0 || reader.ready)) {
+ c = reader.read
if (c >= 0) result.append(c.asInstanceOf[Char])
else done = true
}
if (result.length > 0) {
- put_result(Markup.STDOUT, result.toString)
+ put_result(markup, result.toString)
result.length = 0
}
else {
- process.stdout.close
+ reader.close
finished = true
}
//}}}
--- a/src/Pure/System/session.scala Fri Nov 25 19:07:26 2011 +0100
+++ b/src/Pure/System/session.scala Fri Nov 25 22:21:37 2011 +0100
@@ -23,7 +23,6 @@
//{{{
case object Global_Settings
case object Caret_Focus
- case object Assignment
case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command])
sealed abstract class Phase
@@ -53,7 +52,6 @@
val global_settings = new Event_Bus[Session.Global_Settings.type]
val caret_focus = new Event_Bus[Session.Caret_Focus.type]
- 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 syslog_messages = new Event_Bus[Isabelle_Process.Result]
@@ -82,6 +80,35 @@
//}}}
+ /** pipelined change parsing **/
+
+ //{{{
+ private case class Text_Edits(
+ syntax: Outer_Syntax,
+ name: Document.Node.Name,
+ previous: Future[Document.Version],
+ text_edits: List[Document.Edit_Text],
+ version_result: Promise[Document.Version])
+
+ private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true)
+ {
+ var finished = false
+ while (!finished) {
+ receive {
+ case Stop => finished = true; reply(())
+
+ case Text_Edits(syntax, name, previous, text_edits, version_result) =>
+ val prev = previous.get_finished
+ val (doc_edits, version) = Thy_Syntax.text_edits(syntax, prev, text_edits)
+ version_result.fulfill(version)
+ sender ! Change_Node(name, doc_edits, prev, version)
+
+ case bad => System.err.println("change_parser: ignoring bad message " + bad)
+ }
+ }
+ }
+ //}}}
+
/** main protocol actor **/
@@ -258,15 +285,10 @@
prover.get.cancel_execution()
val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
- val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
- val change =
- global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2)))
+ val version = Future.promise[Document.Version]
+ val change = global_state.change_yield(_.continue_history(previous, text_edits, version))
- result.map {
- case (doc_edits, _) =>
- assignments.await { global_state().is_assigned(previous.get_finished) }
- this_actor ! Change_Node(name, doc_edits, previous.join, change.version.join)
- }
+ change_parser ! Text_Edits(syntax, name, previous, text_edits, version)
}
//}}}
@@ -278,7 +300,6 @@
{
val cmds = global_state.change_yield(_.assign(id, assign))
for (cmd <- cmds) commands_changed_delay.invoke(cmd)
- assignments.event(Session.Assignment)
}
//}}}
@@ -444,9 +465,6 @@
List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
reply(())
- case change: Change_Node if prover.isDefined =>
- handle_change(change)
-
case Messages(msgs) =>
msgs foreach {
case input: Isabelle_Process.Input =>
@@ -455,11 +473,16 @@
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)
+ if (result.is_stdout || result.is_stderr) raw_output_messages.event(result)
raw_messages.event(result)
}
- case bad => System.err.println("session_actor: ignoring bad message " + bad)
+ case change: Change_Node
+ if prover.isDefined && global_state().is_assigned(change.previous) =>
+ handle_change(change)
+
+ case bad if !bad.isInstanceOf[Change_Node] =>
+ System.err.println("session_actor: ignoring bad message " + bad)
}
}
//}}}
@@ -473,7 +496,7 @@
def start(args: List[String]) { start (Time.seconds(25), args) }
- def stop() { commands_changed_buffer !? Stop; session_actor !? Stop }
+ def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
def cancel_execution() { session_actor ! Cancel_Execution }
--- a/src/Pure/sign.ML Fri Nov 25 19:07:26 2011 +0100
+++ b/src/Pure/sign.ML Fri Nov 25 22:21:37 2011 +0100
@@ -149,7 +149,7 @@
val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
val naming = Name_Space.default_naming;
- val syn = Syntax.merge_syntaxes syn1 syn2;
+ val syn = Syntax.merge_syntax (syn1, syn2);
val tsig = Type.merge_tsig ctxt (tsig1, tsig2);
val consts = Consts.merge (consts1, consts2);
in make_sign (naming, syn, tsig, consts) end;
--- a/src/Pure/theory.ML Fri Nov 25 19:07:26 2011 +0100
+++ b/src/Pure/theory.ML Fri Nov 25 22:21:37 2011 +0100
@@ -147,7 +147,7 @@
|> Sign.local_path
|> Sign.map_naming (Name_Space.set_theory_name name)
|> apply_wrappers wrappers
- |> tap (Syntax.join_syntax o Sign.syn_of)
+ |> tap (Syntax.force_syntax o Sign.syn_of)
end;
fun end_theory thy =
--- a/src/Tools/jEdit/etc/settings Fri Nov 25 19:07:26 2011 +0100
+++ b/src/Tools/jEdit/etc/settings Fri Nov 25 22:21:37 2011 +0100
@@ -4,8 +4,8 @@
JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit"
JEDIT_OPTIONS="-reuseview -noserver -nobackground -log=9"
-JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
-#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss1m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
+JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss4m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
+#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit"
JEDIT_STYLE_SHEETS="$ISABELLE_HOME/etc/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Fri Nov 25 19:07:26 2011 +0100
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Fri Nov 25 22:21:37 2011 +0100
@@ -30,7 +30,7 @@
loop {
react {
case result: Isabelle_Process.Result =>
- if (result.is_stdout)
+ if (result.is_stdout || result.is_stderr)
Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)