# HG changeset patch
# User wenzelm
# Date 1322256097 -3600
# Node ID f62edaefff41c041f7e0e9572cdd90455b1419a4
# Parent  efddd75c741e6acfcf4036806c66d608f5604cc5# Parent  202071bb7f8698912c5b117a609f0607bc9da371
merged

diff -r efddd75c741e -r f62edaefff41 src/HOL/MicroJava/J/JBasis.thy
--- 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
diff -r efddd75c741e -r f62edaefff41 src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
--- 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"
diff -r efddd75c741e -r f62edaefff41 src/HOL/Predicate.thy
--- 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"
diff -r efddd75c741e -r f62edaefff41 src/Pure/General/markup.scala
--- 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"
diff -r efddd75c741e -r f62edaefff41 src/Pure/PIDE/text.scala
--- 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
   }
 
diff -r efddd75c741e -r f62edaefff41 src/Pure/Syntax/parser.ML
--- 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;
 
 
 
diff -r efddd75c741e -r f62edaefff41 src/Pure/Syntax/syntax.ML
--- 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)
diff -r efddd75c741e -r f62edaefff41 src/Pure/System/event_bus.scala
--- 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
-  }
 }
diff -r efddd75c741e -r f62edaefff41 src/Pure/System/isabelle_process.scala
--- 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
           }
           //}}}
diff -r efddd75c741e -r f62edaefff41 src/Pure/System/session.scala
--- 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 }
 
diff -r efddd75c741e -r f62edaefff41 src/Pure/sign.ML
--- 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;
diff -r efddd75c741e -r f62edaefff41 src/Pure/theory.ML
--- 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 =
diff -r efddd75c741e -r f62edaefff41 src/Tools/jEdit/etc/settings
--- 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"
diff -r efddd75c741e -r f62edaefff41 src/Tools/jEdit/src/raw_output_dockable.scala
--- 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)