# HG changeset patch
# User wenzelm
# Date 1330609712 -3600
# Node ID b91628b2522b69607a453f5973eb88cedc8dd899
# Parent  a10dcc985e8d70232817a2c7487f36069ad45ecc# Parent  125e49d04cf6cccdf615f474b4a7102d90901989
merged

diff -r a10dcc985e8d -r b91628b2522b lib/scripts/getsettings
--- a/lib/scripts/getsettings	Thu Mar 01 11:28:56 2012 +0100
+++ b/lib/scripts/getsettings	Thu Mar 01 14:48:32 2012 +0100
@@ -55,8 +55,8 @@
 
 #JVM path wrapper
 if [ "$OSTYPE" = cygwin ]; then
-  CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
-  function jvmpath() { cygpath -C UTF8 -w -p "$@"; }
+  CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
+  function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
   THIS_CYGWIN="$(jvmpath "/")"
 else
   function jvmpath() { echo "$@"; }
diff -r a10dcc985e8d -r b91628b2522b src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Thu Mar 01 14:48:32 2012 +0100
@@ -28,8 +28,8 @@
   "list_all' P xs \<equiv> list_all'_rec P 0 xs"
 
 lemma list_all'_rec:
-  "\<And>n. list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
-  apply (induct xs)
+  "list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
+  apply (induct xs arbitrary: n)
   apply auto
   apply (case_tac p)
   apply auto
diff -r a10dcc985e8d -r b91628b2522b src/HOL/MicroJava/Comp/Index.thy
--- a/src/HOL/MicroJava/Comp/Index.thy	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/HOL/MicroJava/Comp/Index.thy	Thu Mar 01 14:48:32 2012 +0100
@@ -127,7 +127,7 @@
 lemma wf_java_mdecl_disjoint_varnames: 
   "wf_java_mdecl G C (S,rT,(pns,lvars,blk,res)) 
   \<Longrightarrow> disjoint_varnames pns lvars"
-apply (case_tac S)
+apply (cases S)
 apply (simp add: wf_java_mdecl_def disjoint_varnames_def  map_of_in_set)
 done
 
diff -r a10dcc985e8d -r b91628b2522b src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Mar 01 14:48:32 2012 +0100
@@ -212,15 +212,15 @@
         |> touch_node name
     | Header header =>
         let
-          val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
+          val imports = (case header of Exn.Res (_, imports, _) => imports | _ => []);
           val nodes1 = nodes
             |> default_node name
-            |> fold default_node parents;
+            |> fold default_node imports;
           val nodes2 = nodes1
             |> Graph.Keys.fold
                 (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
           val (header', nodes3) =
-            (header, Graph.add_deps_acyclic (name, parents) nodes2)
+            (header, Graph.add_deps_acyclic (name, imports) nodes2)
               handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
         in Graph.map_node name (set_header header') nodes3 end
         |> touch_node name
diff -r a10dcc985e8d -r b91628b2522b src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Mar 01 14:48:32 2012 +0100
@@ -35,10 +35,12 @@
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
   type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
 
-  type Node_Header = Exn.Result[Thy_Header]
+  type Node_Header = Exn.Result[Node.Deps]
 
   object Node
   {
+    sealed case class Deps(imports: List[Name], uses: List[(String, Boolean)])
+
     object Name
     {
       val empty = Name("", "", "")
@@ -81,12 +83,6 @@
     case class Header[A, B](header: Node_Header) extends Edit[A, B]
     case class Perspective[A, B](perspective: B) extends Edit[A, B]
 
-    def norm_header(f: String => String, g: String => String, header: Node_Header): Node_Header =
-      header match {
-        case Exn.Res(h) => Exn.capture { h.norm_deps(f, g) }
-        case exn => exn
-      }
-
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
     {
@@ -192,17 +188,15 @@
     def + (entry: (Node.Name, Node)): Nodes =
     {
       val (name, node) = entry
-      val parents =
+      val imports =
         node.header match {
-          case Exn.Res(header) =>
-            // FIXME official names of yet unknown nodes!?
-            for (imp <- header.imports; imp_name <- get_name(imp)) yield imp_name
+          case Exn.Res(deps) => deps.imports
           case _ => Nil
         }
       val graph1 =
-        (graph.default_node(name, Node.empty) /: parents)((g, p) => g.default_node(p, Node.empty))
+        (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
       val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
-      val graph3 = (graph2 /: parents)((g, dep) => g.add_edge(dep, name))
+      val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name))
       new Nodes(graph3.map_node(name, _ => node))
     }
 
diff -r a10dcc985e8d -r b91628b2522b src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Thu Mar 01 14:48:32 2012 +0100
@@ -211,22 +211,24 @@
     val edits_yxml =
     { import XML.Encode._
       def id: T[Command] = (cmd => long(cmd.id))
-      def encode_edit(dir: String)
+      def encode_edit(name: Document.Node.Name)
           : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
         variant(List(
           { case Document.Node.Clear() => (Nil, Nil) },
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
-          { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
+          { case Document.Node.Header(Exn.Res(deps)) =>
+              val dir = Isabelle_System.posix_path(name.dir)
+              val imports = deps.imports.map(_.node)
+              val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
               (Nil,
                 triple(pair(string, string), list(string), list(pair(string, bool)))(
-                  (dir, a), b, c)) },
+                  (dir, name.theory), imports, uses)) },
           { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
           { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
       def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
       {
         val (name, edit) = node_edit
-        val dir = Isabelle_System.posix_path(name.dir)
-        pair(string, encode_edit(dir))(name.node, edit)
+        pair(string, encode_edit(name))(name.node, edit)
       })
       YXML.string_of_body(encode(edits)) }
     input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
diff -r a10dcc985e8d -r b91628b2522b src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Mar 01 14:48:32 2012 +0100
@@ -143,7 +143,7 @@
       Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
         handle ERROR msg =>
           (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
-            tell_file_retracted (Thy_Header.thy_path name))
+            tell_file_retracted (Thy_Load.thy_path (Path.basic name)))
     val _ = Isar.init ();
   in () end;
 
diff -r a10dcc985e8d -r b91628b2522b src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/System/session.scala	Thu Mar 01 14:48:32 2012 +0100
@@ -143,20 +143,11 @@
 
   def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text =
   {
-    def norm_import(s: String): String =
-    {
-      val thy_name = Thy_Header.base_name(s)
-      if (thy_load.is_loaded(thy_name)) thy_name
-      else thy_load.append(name.dir, Thy_Header.thy_path(Path.explode(s)))
-    }
-    def norm_use(s: String): String = thy_load.append(name.dir, Path.explode(s))
-
     val header1: Document.Node_Header =
       header match {
-        case Exn.Res(Thy_Header(thy_name, _, _))
-        if (thy_load.is_loaded(thy_name)) =>
-          Exn.Exn(ERROR("Attempt to update loaded theory " + quote(thy_name)))
-        case _ => Document.Node.norm_header(norm_import, norm_use, header)
+        case Exn.Res(_) if (thy_load.is_loaded(name.theory)) =>
+          Exn.Exn(ERROR("Attempt to update loaded theory " + quote(name.theory)))
+        case _ => header
       }
     (name, Document.Node.Header(header1))
   }
diff -r a10dcc985e8d -r b91628b2522b src/Pure/System/swing_thread.scala
--- a/src/Pure/System/swing_thread.scala	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/System/swing_thread.scala	Thu Mar 01 14:48:32 2012 +0100
@@ -45,7 +45,7 @@
 
   /* delayed actions */
 
-  private def delayed_action(first: Boolean)(time: Time)(action: => Unit): () => Unit =
+  private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Boolean => Unit =
   {
     val listener = new ActionListener {
       override def actionPerformed(e: ActionEvent) { Swing_Thread.assert(); action }
@@ -54,7 +54,9 @@
     timer.setRepeats(false)
 
     def invoke() { later { if (first) timer.start() else timer.restart() } }
-    invoke _
+    def revoke() { timer.stop() }
+
+    (active: Boolean) => if (active) invoke() else revoke()
   }
 
   // delayed action after first invocation
diff -r a10dcc985e8d -r b91628b2522b src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/Thy/thy_header.ML	Thu Mar 01 14:48:32 2012 +0100
@@ -8,8 +8,6 @@
 sig
   val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
   val read: Position.T -> string -> string * string list * (Path.T * bool) list
-  val thy_path: string -> Path.T
-  val consistent_name: string -> string -> unit
 end;
 
 structure Thy_Header: THY_HEADER =
@@ -67,13 +65,4 @@
     | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
   end;
 
-
-(* file name *)
-
-val thy_path = Path.ext "thy" o Path.basic;
-
-fun consistent_name name name' =
-  if name = name' then ()
-  else error ("Bad file name " ^ Path.print (thy_path name) ^ " for theory " ^ quote name');
-
 end;
diff -r a10dcc985e8d -r b91628b2522b src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/Thy/thy_header.scala	Thu Mar 01 14:48:32 2012 +0100
@@ -37,8 +37,6 @@
   def thy_name(s: String): Option[String] =
     s match { case Thy_Name(name) => Some(name) case _ => None }
 
-  def thy_path(path: Path): Path = path.ext("thy")
-
 
   /* header */
 
@@ -96,18 +94,6 @@
     try { read(reader).map(Standard_System.decode_permissive_utf8) }
     finally { reader.close }
   }
-
-
-  /* check */
-
-  def check(name: String, source: CharSequence): Thy_Header =
-  {
-    val header = read(source)
-    val name1 = header.name
-    val path = Path.explode(name)
-    if (name != name1) error("Bad file name " + thy_path(path) + " for theory " + quote(name1))
-    header
-  }
 }
 
 
@@ -116,10 +102,5 @@
 {
   def map(f: String => String): Thy_Header =
     Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
-
-  def norm_deps(f: String => String, g: String => String): Thy_Header =
-    copy(imports = imports.map(name => f(name)))
-    // FIXME
-    // copy(imports = imports.map(name => f(name)), uses = uses.map(p => (g(p._1), p._2)))
 }
 
diff -r a10dcc985e8d -r b91628b2522b src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/Thy/thy_info.scala	Thu Mar 01 14:48:32 2012 +0100
@@ -24,15 +24,6 @@
 
   /* dependencies */
 
-  def import_name(dir: String, str: String): Document.Node.Name =
-  {
-    val path = Path.explode(str)
-    val node = thy_load.append(dir, Thy_Header.thy_path(path))
-    val dir1 = thy_load.append(dir, path.dir)
-    val theory = path.base.implode
-    Document.Node.Name(node, dir1, theory)
-  }
-
   type Dep = (Document.Node.Name, Document.Node_Header)
   private type Required = (List[Dep], Set[Document.Node.Name])
 
@@ -49,16 +40,16 @@
     else {
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
-        val header =
+        val node_deps =
           try { thy_load.check_thy(name) }
           catch {
             case ERROR(msg) =>
               cat_error(msg, "The error(s) above occurred while examining theory " +
                 quote(name.theory) + required_by(initiators))
           }
-        val imports = header.imports.map(import_name(name.dir, _))
-        val (deps1, seen1) = require_thys(name :: initiators, (deps, seen + name), imports)
-        ((name, Exn.Res(header)) :: deps1, seen1)
+        val (deps1, seen1) =
+          require_thys(name :: initiators, (deps, seen + name), node_deps.imports)
+        ((name, Exn.Res(node_deps)) :: deps1, seen1)
       }
       catch { case e: Throwable => (((name, Exn.Exn(e)): Dep) :: deps, seen + name) }
     }
diff -r a10dcc985e8d -r b91628b2522b src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/Thy/thy_load.ML	Thu Mar 01 14:48:32 2012 +0100
@@ -10,6 +10,7 @@
   val imports_of: theory -> string list
   val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory
   val check_file: Path.T -> Path.T -> Path.T
+  val thy_path: Path.T -> Path.T
   val check_thy: Path.T -> string ->
     {master: Path.T * SHA1.digest, text: string, imports: string list, uses: (Path.T * bool) list}
   val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
@@ -75,14 +76,18 @@
 
 fun check_file dir file = File.check_file (File.full_path dir file);
 
+val thy_path = Path.ext "thy";
+
 fun check_thy dir name =
   let
-    val master_file = check_file dir (Thy_Header.thy_path name);
+    val path = thy_path (Path.basic name);
+    val master_file = check_file dir path;
     val text = File.read master_file;
     val (name', imports, uses) =
       if name = Context.PureN then (Context.PureN, [], [])
       else Thy_Header.read (Path.position master_file) text;
-    val _ = Thy_Header.consistent_name name name';
+    val _ = name <> name' andalso
+      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name');
   in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end;
 
 
diff -r a10dcc985e8d -r b91628b2522b src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala	Thu Mar 01 14:48:32 2012 +0100
@@ -29,11 +29,39 @@
   def append(dir: String, source_path: Path): String =
     (Path.explode(dir) + source_path).implode
 
-  def check_thy(name: Document.Node.Name): Thy_Header =
+  def read_header(name: Document.Node.Name): Thy_Header =
   {
     val file = new File(name.node)
     if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
     Thy_Header.read(file)
   }
+
+
+  /* theory files */
+
+  def thy_path(path: Path): Path = path.ext("thy")
+
+  private def import_name(dir: String, s: String): Document.Node.Name =
+  {
+    val theory = Thy_Header.base_name(s)
+    if (is_loaded(theory)) Document.Node.Name(theory, "", theory)
+    else {
+      val path = Path.explode(s)
+      val node = append(dir, thy_path(path))
+      val dir1 = append(dir, path.dir)
+      Document.Node.Name(node, dir1, theory)
+    }
+  }
+
+  def check_thy(name: Document.Node.Name): Document.Node.Deps =
+  {
+    val header = read_header(name)
+    val name1 = header.name
+    val imports = header.imports.map(import_name(name.dir, _))
+    val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
+    if (name.theory != name1)
+      error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1))
+    Document.Node.Deps(imports, uses)
+  }
 }
 
diff -r a10dcc985e8d -r b91628b2522b src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Mar 01 14:48:32 2012 +0100
@@ -258,7 +258,7 @@
           val node = nodes(name)
           val update_header =
             (node.header, header) match {
-              case (Exn.Res(thy_header0), Exn.Res(thy_header)) => thy_header0 != thy_header
+              case (Exn.Res(deps0), Exn.Res(deps)) => deps != deps
               case _ => true
             }
           if (update_header) {
diff -r a10dcc985e8d -r b91628b2522b src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Tools/Code/code_runtime.ML	Thu Mar 01 14:48:32 2012 +0100
@@ -310,8 +310,9 @@
   | process_reflection (code, _) _ (SOME file_name) thy =
       let
         val preamble =
-          "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
-          ^ "; DO NOT EDIT! *)";
+          "(* Generated from " ^
+            Path.implode (Thy_Load.thy_path (Path.basic (Context.theory_name thy))) ^
+          "; DO NOT EDIT! *)";
         val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code);
       in
         thy
diff -r a10dcc985e8d -r b91628b2522b src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Mar 01 14:48:32 2012 +0100
@@ -60,10 +60,12 @@
 {
   /* header */
 
-  def node_header(): Exn.Result[Thy_Header] =
+  def node_header(): Document.Node_Header =
   {
     Swing_Thread.require()
-    Exn.capture { Thy_Header.check(name.theory, buffer.getSegment(0, buffer.getLength)) }
+    if (Isabelle.jedit_buffer(name.node) == Some(buffer))
+      Exn.capture { Isabelle.thy_load.check_thy(name) }
+    else Exn.Exn(ERROR("Bad theory header"))  // FIXME odd race condition!?
   }
 
 
@@ -109,12 +111,6 @@
       }
     }
 
-    def init()
-    {
-      flush()
-      session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
-    }
-
     private val delay_flush =
       Swing_Thread.delay_last(session.input_delay) { flush() }
 
@@ -122,13 +118,25 @@
     {
       Swing_Thread.require()
       pending += edit
-      delay_flush()
+      delay_flush(true)
     }
 
     def update_perspective()
     {
       pending_perspective = true
-      delay_flush()
+      delay_flush(true)
+    }
+
+    def init()
+    {
+      flush()
+      session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
+    }
+
+    def exit()
+    {
+      delay_flush(false)
+      flush()
     }
   }
 
@@ -190,7 +198,7 @@
 
   private def deactivate()
   {
-    pending_edits.flush()
+    pending_edits.exit()
     buffer.removeBufferListener(buffer_listener)
     Token_Markup.refresh_buffer(buffer)
   }
diff -r a10dcc985e8d -r b91628b2522b src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Mar 01 14:48:32 2012 +0100
@@ -343,11 +343,13 @@
     update_snapshot().node.proper_command_at(text_area.getCaretPosition)
   }
 
-  private val caret_listener = new CaretListener {
-    private val delay = Swing_Thread.delay_last(session.input_delay) {
+  private val delay_caret_update =
+    Swing_Thread.delay_last(session.input_delay) {
       session.caret_focus.event(Session.Caret_Focus)
     }
-    override def caretUpdate(e: CaretEvent) { delay() }
+
+  private val caret_listener = new CaretListener {
+    override def caretUpdate(e: CaretEvent) { delay_caret_update(true) }
   }
 
 
@@ -373,7 +375,7 @@
             if (updated ||
                 (changed.nodes.contains(model.name) &&
                  changed.commands.exists(snapshot.node.commands.contains)))
-              overview.delay_repaint()
+              overview.delay_repaint(true)
 
             visible_range() match {
               case None =>
@@ -430,8 +432,8 @@
     text_area.removeFocusListener(focus_listener)
     text_area.getView.removeWindowListener(window_listener)
     painter.removeMouseMotionListener(mouse_motion_listener)
-    text_area.removeCaretListener(caret_listener)
-    text_area.removeLeftOfScrollBar(overview)
+    text_area.removeCaretListener(caret_listener); delay_caret_update(false)
+    text_area.removeLeftOfScrollBar(overview); overview.delay_repaint(false)
     text_area.getGutter.removeExtension(gutter_painter)
     text_area_painter.deactivate()
     painter.removeExtension(tooltip_painter)
diff -r a10dcc985e8d -r b91628b2522b src/Tools/jEdit/src/jedit_thy_load.scala
--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Thu Mar 01 14:48:32 2012 +0100
@@ -52,7 +52,7 @@
     }
   }
 
-  override def check_thy(name: Document.Node.Name): Thy_Header =
+  override def read_header(name: Document.Node.Name): Thy_Header =
   {
     Swing_Thread.now {
       Isabelle.jedit_buffer(name.node) match {
diff -r a10dcc985e8d -r b91628b2522b src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Mar 01 14:48:32 2012 +0100
@@ -126,14 +126,17 @@
     Isabelle.session.global_settings -= main_actor
     Isabelle.session.commands_changed -= main_actor
     Isabelle.session.caret_focus -= main_actor
+    delay_resize(false)
   }
 
 
   /* resize */
 
+  private val delay_resize =
+    Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
+
   addComponentListener(new ComponentAdapter {
-    val delay = Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
-    override def componentResized(e: ComponentEvent) { delay() }
+    override def componentResized(e: ComponentEvent) { delay_resize(true) }
   })
 
 
diff -r a10dcc985e8d -r b91628b2522b src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Mar 01 14:48:32 2012 +0100
@@ -390,9 +390,12 @@
 
             case Session.Ready =>
               Isabelle.jedit_buffers.foreach(Isabelle.init_model)
-              delay_load()
+              delay_load(true)
 
-            case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
+            case Session.Shutdown =>
+              Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
+              delay_load(false)
+
             case _ =>
           }
         case bad => System.err.println("session_manager: ignoring bad message " + bad)
@@ -416,7 +419,7 @@
         if (Isabelle.session.is_ready) {
           val buffer = msg.getBuffer
           if (buffer != null) Isabelle.init_model(buffer)
-          delay_load()
+          delay_load(true)
         }
 
       case msg: EditPaneUpdate
diff -r a10dcc985e8d -r b91628b2522b src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala	Thu Mar 01 14:48:32 2012 +0100
@@ -155,7 +155,8 @@
         }
       val nodes_status1 =
         (nodes_status /: iterator)({ case (status, (name, node)) =>
-            status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
+            if (Isabelle.thy_load.is_loaded(name.theory)) status
+            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
 
       if (nodes_status != nodes_status1) {
         nodes_status = nodes_status1