# HG changeset patch
# User wenzelm
# Date 1344371534 -7200
# Node ID 9775c2957000a4ad51f2aa5524ea8f45f01b2b50
# Parent  1d2a12bb0640e37dcae63af419a43ac92f64dbbf# Parent  73e6c22e2d949a283fe9f23bed47efb0a575884c
merged

diff -r 1d2a12bb0640 -r 9775c2957000 Admin/update-keywords
--- a/Admin/update-keywords	Tue Aug 07 14:29:18 2012 +0200
+++ b/Admin/update-keywords	Tue Aug 07 22:32:14 2012 +0200
@@ -11,10 +11,8 @@
 cd "$ISABELLE_HOME/etc"
 
 isabelle keywords \
-  "$LOG/Pure.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" \
-  "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" "$LOG/HOL-Statespace.gz" \
-  "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz" "$LOG/HOL-Import.gz"
+  "$LOG/HOLCF.gz" "$LOG/HOL-Boogie.gz" "$LOG/HOL-Library.gz" "$LOG/HOL-Nominal.gz" \
+  "$LOG/HOL-Statespace.gz" "$LOG/HOL-SPARK.gz" "$LOG/HOL-TPTP.gz" "$LOG/HOL-Import.gz"
 
-isabelle keywords -k ZF \
-  "$LOG/Pure.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
+isabelle keywords -k ZF "$LOG/ZF.gz"
 
diff -r 1d2a12bb0640 -r 9775c2957000 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Tue Aug 07 14:29:18 2012 +0200
+++ b/etc/isar-keywords-ZF.el	Tue Aug 07 22:32:14 2012 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + FOL + ZF.
+;; Generated from ZF.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
diff -r 1d2a12bb0640 -r 9775c2957000 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Tue Aug 07 14:29:18 2012 +0200
+++ b/etc/isar-keywords.el	Tue Aug 07 22:32:14 2012 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import.
+;; Generated from HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-Import.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/General/pretty.ML	Tue Aug 07 22:32:14 2012 +0200
@@ -21,6 +21,7 @@
 
 signature PRETTY =
 sig
+  val spaces: int -> string
   val default_indent: string -> int -> Output.output
   val add_mode: string -> (string -> int -> Output.output) -> unit
   type T
@@ -69,9 +70,22 @@
 structure Pretty: PRETTY =
 struct
 
+(** spaces **)
+
+local
+  val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i Symbol.space);
+in
+  fun spaces k =
+    if k < 64 then Vector.sub (small_spaces, k)
+    else Library.replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
+      Vector.sub (small_spaces, k mod 64);
+end;
+
+
+
 (** print mode operations **)
 
-fun default_indent (_: string) = Symbol.spaces;
+fun default_indent (_: string) = spaces;
 
 local
   val default = {indent = default_indent};
@@ -89,7 +103,7 @@
 
 fun mode_indent x y = #indent (get_mode ()) x y;
 
-val output_spaces = Output.output o Symbol.spaces;
+val output_spaces = Output.output o spaces;
 val add_indent = Buffer.add o output_spaces;
 
 
@@ -167,7 +181,7 @@
 fun big_list name prts = block (fbreaks (str name :: prts));
 
 fun indent 0 prt = prt
-  | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
+  | indent n prt = blk (0, [str (spaces n), prt]);
 
 fun unbreakable (Break (_, wd)) = String (output_spaces wd, wd)
   | unbreakable (Block (m, es, indent, wd)) = Block (m, map unbreakable es, indent, wd)
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/General/pretty.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -12,6 +12,21 @@
 
 object Pretty
 {
+  /* spaces */
+
+  val spc = ' '
+  val space = " "
+
+  private val static_spaces = space * 4000
+
+  def spaces(k: Int): String =
+  {
+    require(k >= 0)
+    if (k < static_spaces.length) static_spaces.substring(0, k)
+    else space * k
+  }
+
+
   /* markup trees with physical blocks and breaks */
 
   def block(body: XML.Body): XML.Tree = Block(2, body)
@@ -33,7 +48,7 @@
   {
     def apply(w: Int): XML.Tree =
       XML.Elem(Markup(Isabelle_Markup.BREAK, Isabelle_Markup.Width(w)),
-        List(XML.Text(Symbol.spaces(w))))
+        List(XML.Text(spaces(w))))
 
     def unapply(tree: XML.Tree): Option[Int] =
       tree match {
@@ -59,7 +74,7 @@
   {
     def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
     def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
-    def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
+    def blanks(wd: Int): Text = string(spaces(wd), wd.toDouble)
     def content: XML.Body = tx.reverse
   }
 
@@ -69,7 +84,7 @@
   def font_metric(metrics: FontMetrics): String => Double =
     if (metrics == null) ((s: String) => s.length.toDouble)
     else {
-      val unit = metrics.charWidth(Symbol.spc).toDouble
+      val unit = metrics.charWidth(spc).toDouble
       ((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
     }
 
@@ -143,8 +158,8 @@
     def fmt(tree: XML.Tree): XML.Body =
       tree match {
         case Block(_, body) => body.flatMap(fmt)
-        case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
-        case FBreak => List(XML.Text(Symbol.space))
+        case Break(wd) => List(XML.Text(spaces(wd)))
+        case FBreak => List(XML.Text(space))
         case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
         case XML.Text(_) => List(tree)
       }
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/General/symbol.ML	Tue Aug 07 22:32:14 2012 +0200
@@ -10,7 +10,6 @@
   val STX: symbol
   val DEL: symbol
   val space: symbol
-  val spaces: int -> string
   val is_char: symbol -> bool
   val is_utf8: symbol -> bool
   val is_symbolic: symbol -> bool
@@ -92,15 +91,6 @@
 
 val space = chr 32;
 
-local
-  val small_spaces = Vector.tabulate (65, fn i => Library.replicate_string i space);
-in
-  fun spaces k =
-    if k < 64 then Vector.sub (small_spaces, k)
-    else Library.replicate_string (k div 64) (Vector.sub (small_spaces, 64)) ^
-      Vector.sub (small_spaces, k mod 64);
-end;
-
 fun is_char s = size s = 1;
 
 fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/General/symbol.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -15,21 +15,6 @@
   type Symbol = String
 
 
-  /* spaces */
-
-  val spc = ' '
-  val space = " "
-
-  private val static_spaces = space * 4000
-
-  def spaces(k: Int): String =
-  {
-    require(k >= 0)
-    if (k < static_spaces.length) static_spaces.substring(0, k)
-    else space * k
-  }
-
-
   /* ASCII characters */
 
   def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'
@@ -345,7 +330,7 @@
       "\\<^isub>", "\\<^isup>")
 
     val blanks =
-      recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<spacespace>", "\\<^newline>")
+      recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<spacespace>", "\\<^newline>")
 
     val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Isar/keyword.ML	Tue Aug 07 22:32:14 2012 +0200
@@ -49,7 +49,6 @@
   val command_keyword: string -> T option
   val command_tags: string -> string list
   val dest: unit -> string list * string list
-  val keyword_statusN: string
   val status: unit -> unit
   val define: string * T option -> unit
   val is_diag: string -> bool
@@ -183,43 +182,29 @@
 
 (* status *)
 
-val keyword_statusN = "keyword_status";
-
-fun status_message m s =
-  Position.setmp_thread_data Position.none
-    (if print_mode_active keyword_statusN then Output.protocol_message m else writeln) s;
-
-fun keyword_status name =
-  status_message (Isabelle_Markup.keyword_decl name)
-    ("Outer syntax keyword " ^ quote name);
-
-fun command_status (name, kind) =
-  status_message (Isabelle_Markup.command_decl name (kind_of kind))
-    ("Outer syntax keyword " ^ quote name ^ " :: " ^ kind_of kind);
-
 fun status () =
   let
     val {lexicons = (minor, _), commands} = get_keywords ();
-    val _ = List.app keyword_status (sort_strings (Scan.dest_lexicon minor));
-    val _ = List.app command_status (sort_wrt #1 (Symtab.dest commands));
+    val _ = sort_strings (Scan.dest_lexicon minor) |> List.app (fn name =>
+      writeln ("Outer syntax keyword " ^ quote name));
+    val _ = sort_wrt #1 (Symtab.dest commands) |> List.app (fn (name, kind) =>
+      writeln ("Outer syntax keyword " ^ quote name ^ " :: " ^ kind_of kind));
   in () end;
 
 
 (* define *)
 
-fun define (name, NONE) =
-     (change_keywords (fn ((minor, major), commands) =>
-        let
-          val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
-        in ((minor', major), commands) end);
-      keyword_status name)
-  | define (name, SOME kind) =
-     (change_keywords (fn ((minor, major), commands) =>
-        let
-          val major' = Scan.extend_lexicon (Symbol.explode name) major;
-          val commands' = Symtab.update (name, kind) commands;
-        in ((minor, major'), commands') end);
-      command_status (name, kind));
+fun define (name, opt_kind) = change_keywords (fn ((minor, major), commands) =>
+  (case opt_kind of
+    NONE =>
+      let
+        val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
+      in ((minor', major), commands) end
+  | SOME kind =>
+      let
+        val major' = Scan.extend_lexicon (Symbol.explode name) major;
+        val commands' = Symtab.update (name, kind) commands;
+      in ((minor, major'), commands') end));
 
 
 (* command categories *)
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -34,8 +34,6 @@
     result.toString
   }
 
-  type Decl = (String, Option[(String, List[String])])
-
   val empty: Outer_Syntax = new Outer_Syntax()
   def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
 }
@@ -61,10 +59,13 @@
 
   def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
   def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
-  def + (decl: Outer_Syntax.Decl): Outer_Syntax =
-    decl match {
-      case ((name, Some((kind, _)))) => this + (name, kind)
-      case ((name, None)) => this + name
+
+  def add_keywords(header: Document.Node.Header): Outer_Syntax =
+    (this /: header.keywords) {
+      case (syntax, ((name, Some((kind, _))))) =>
+        syntax + (Symbol.decode(name), kind) + (Symbol.encode(name), kind)
+      case (syntax, ((name, None))) =>
+        syntax + Symbol.decode(name) + Symbol.encode(name)
     }
 
   def is_command(name: String): Boolean =
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Isar/parse.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -50,9 +50,11 @@
     def atom(s: String, pred: Elem => Boolean): Parser[String] =
       token(s, pred) ^^ (_.content)
 
+    def command(name: String): Parser[String] =
+      atom("command " + quote(name), tok => tok.is_command && tok.source == name)
+
     def keyword(name: String): Parser[String] =
-      atom(Token.Kind.KEYWORD.toString + " " + quote(name),
-        tok => tok.kind == Token.Kind.KEYWORD && tok.content == name)
+      atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
 
     def string: Parser[String] = atom("string", _.is_string)
     def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Isar/token.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -67,7 +67,8 @@
 sealed case class Token(val kind: Token.Kind.Value, val source: String)
 {
   def is_command: Boolean = kind == Token.Kind.COMMAND
-  def is_operator: Boolean = kind == Token.Kind.KEYWORD && !Symbol.is_ascii_identifier(source)
+  def is_keyword: Boolean = kind == Token.Kind.KEYWORD
+  def is_operator: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
   def is_delimited: Boolean =
     kind == Token.Kind.STRING ||
     kind == Token.Kind.ALT_STRING ||
@@ -90,8 +91,8 @@
   def is_proper: Boolean = !is_space && !is_comment
   def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
 
-  def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin"
-  def is_end: Boolean = kind == Token.Kind.COMMAND && source == "end"
+  def is_begin: Boolean = is_keyword && source == "begin"
+  def is_end: Boolean = is_keyword && source == "end"
 
   def content: String =
     if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
@@ -101,7 +102,7 @@
     else source
 
   def text: (String, String) =
-    if (kind == Token.Kind.COMMAND && source == ";") ("terminator", "")
+    if (is_command && source == ";") ("terminator", "")
     else (kind.toString, source)
 }
 
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -133,7 +133,7 @@
   def is_command: Boolean = !is_ignored && !is_malformed
 
   def name: String =
-    span.find(_.is_command) match { case Some(tok) => tok.content case _ => "" }
+    span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
 
   override def toString =
     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Aug 07 22:32:14 2012 +0200
@@ -15,11 +15,11 @@
   val new_id: unit -> id
   val parse_id: string -> id
   val print_id: id -> string
-  type node_header = (string * Thy_Header.header) Exn.result
+  type node_header = string * Thy_Header.header * string list
   datatype node_edit =
     Clear |
     Edits of (command_id option * command_id option) list |
-    Header of node_header |
+    Deps of node_header |
     Perspective of command_id list
   type edit = string * node_edit
   type state
@@ -59,7 +59,7 @@
 
 (** document structure **)
 
-type node_header = (string * Thy_Header.header) Exn.result;
+type node_header = string * Thy_Header.header * string list;
 type perspective = (command_id -> bool) * command_id option;
 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
 
@@ -67,7 +67,7 @@
 val no_exec = Command.memo_value (Toplevel.toplevel, Lazy.value ());
 
 abstype node = Node of
- {header: node_header,
+ {header: node_header,  (*master directory, theory header, errors*)
   perspective: perspective,  (*visible commands, last*)
   entries: (exec_id * exec) option Entries.T,  (*command entries with excecutions*)
   result: exec option}  (*result of last execution*)
@@ -83,7 +83,7 @@
 fun make_perspective command_ids : perspective =
   (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
 
-val no_header = Exn.Exn (ERROR "Bad theory header");
+val no_header = ("", Thy_Header.make "" [] [] [], ["Bad theory header"]);
 val no_perspective = make_perspective [];
 
 val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
@@ -92,7 +92,10 @@
 
 (* basic components *)
 
-fun get_header (Node {header, ...}) = header;
+fun get_header (Node {header = (master, header, errors), ...}) =
+  if null errors then (master, header)
+  else error (cat_lines errors);
+
 fun set_header header =
   map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
 
@@ -128,7 +131,7 @@
 datatype node_edit =
   Clear |
   Edits of (command_id option * command_id option) list |
-  Header of node_header |
+  Deps of node_header |
   Perspective of command_id list;
 
 type edit = string * node_edit;
@@ -178,22 +181,21 @@
     (case node_edit of
       Clear => update_node name clear_node nodes
     | Edits edits => update_node name (edit_node edits) nodes
-    | Header header =>
+    | Deps (master, header, errors) =>
         let
-          val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
-          val header' =
-            ((case header of Exn.Res (_, h) => Thy_Header.define_keywords h | _ => ()); header)
-              handle exn as ERROR _ => Exn.Exn exn;
+          val errors1 =
+            (Thy_Header.define_keywords header; errors)
+              handle ERROR msg => errors @ [msg];
           val nodes1 = nodes
             |> default_node name
-            |> fold default_node imports;
+            |> fold default_node (#imports header);
           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, 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
+          val (nodes3, errors2) =
+            (Graph.add_deps_acyclic (name, #imports header) nodes2, errors1)
+              handle Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
+        in Graph.map_node name (set_header (master, header, errors2)) nodes3 end
     | Perspective perspective => update_node name (set_perspective perspective) nodes);
 
 fun put_node (name, node) (Version nodes) =
@@ -374,7 +376,7 @@
 fun init_theory imports node =
   let
     (* FIXME provide files via Scala layer, not master_dir *)
-    val (dir, header) = Exn.release (get_header node);
+    val (dir, header) = get_header node;
     val master_dir =
       (case Url.explode dir of
         Url.File path => path
@@ -393,7 +395,7 @@
 
 fun check_theory full name node =
   is_some (Thy_Info.lookup_theory name) orelse
-  is_some (Exn.get_res (get_header node)) andalso (not full orelse is_some (get_result node));
+  can get_header node andalso (not full orelse is_some (get_result node));
 
 fun last_common state last_visible node0 node =
   let
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -35,14 +35,18 @@
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
   type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
 
-  type Node_Header = Exn.Result[Node.Deps]
-
   object Node
   {
-    sealed case class Deps(
+    sealed case class Header(
       imports: List[Name],
-      keywords: List[Outer_Syntax.Decl],
-      uses: List[(String, Boolean)])
+      keywords: Thy_Header.Keywords,
+      uses: List[(String, Boolean)],
+      errors: List[String] = Nil)
+    {
+      def error(msg: String): Header = copy(errors = errors ::: List(msg))
+    }
+
+    def bad_header(msg: String): Header = Header(Nil, Nil, Nil, List(msg))
 
     object Name
     {
@@ -83,7 +87,7 @@
     }
     case class Clear[A, B]() extends Edit[A, B]
     case class Edits[A, B](edits: List[A]) extends Edit[A, B]
-    case class Header[A, B](header: Node_Header) extends Edit[A, B]
+    case class Deps[A, B](header: Header) extends Edit[A, B]
     case class Perspective[A, B](perspective: B) extends Edit[A, B]
 
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
@@ -103,14 +107,14 @@
   }
 
   final class Node private(
-    val header: Node_Header = Exn.Exn(ERROR("Bad theory header")),
+    val header: Node.Header = Node.bad_header("Bad theory header"),
     val perspective: Command.Perspective = Command.Perspective.empty,
     val blobs: Map[String, Blob] = Map.empty,
     val commands: Linear_Set[Command] = Linear_Set.empty)
   {
     def clear: Node = new Node(header = header)
 
-    def update_header(new_header: Node_Header): Node =
+    def update_header(new_header: Node.Header): Node =
       new Node(new_header, perspective, blobs, commands)
 
     def update_perspective(new_perspective: Command.Perspective): Node =
@@ -122,12 +126,6 @@
     def update_commands(new_commands: Linear_Set[Command]): Node =
       new Node(header, perspective, blobs, new_commands)
 
-    def imports: List[Node.Name] =
-      header match { case Exn.Res(deps) => deps.imports case _ => Nil }
-
-    def keywords: List[Outer_Syntax.Decl] =
-      header match { case Exn.Res(deps) => deps.keywords case _ => Nil }
-
 
     /* commands */
 
@@ -190,7 +188,7 @@
     def + (entry: (Node.Name, Node)): Nodes =
     {
       val (name, node) = entry
-      val imports = node.imports
+      val imports = node.header.imports
       val graph1 =
         (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))
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML	Tue Aug 07 22:32:14 2012 +0200
@@ -102,10 +102,6 @@
   val no_reportN: string val no_report: Markup.T
   val badN: string val bad: Markup.T
   val functionN: string
-  val ready: Properties.T
-  val loaded_theory: string -> Properties.T
-  val keyword_decl: string -> Properties.T
-  val command_decl: string -> string -> Properties.T
   val assign_execs: Properties.T
   val removed_versions: Properties.T
   val invoke_scala: string -> string -> Properties.T
@@ -308,14 +304,6 @@
 
 val functionN = "function"
 
-val ready = [(functionN, "ready")];
-
-fun loaded_theory name = [(functionN, "loaded_theory"), (Markup.nameN, name)];
-
-fun keyword_decl name = [(functionN, "keyword_decl"), (Markup.nameN, name)];
-fun command_decl name kind =
-  [(functionN, "command_decl"), (Markup.nameN, name), (Markup.kindN, kind)];
-
 val assign_execs = [(functionN, "assign_execs")];
 val removed_versions = [(functionN, "removed_versions")];
 
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -250,35 +250,6 @@
   val FUNCTION = "function"
   val Function = new Properties.String(FUNCTION)
 
-  val Ready: Properties.T = List((FUNCTION, "ready"))
-
-  object Loaded_Theory
-  {
-    def unapply(props: Properties.T): Option[String] =
-      props match {
-        case List((FUNCTION, "loaded_theory"), (Markup.NAME, name)) => Some(name)
-        case _ => None
-      }
-  }
-
-  object Keyword_Decl
-  {
-    def unapply(props: Properties.T): Option[String] =
-      props match {
-        case List((FUNCTION, "keyword_decl"), (Markup.NAME, name)) => Some(name)
-        case _ => None
-      }
-  }
-  object Command_Decl
-  {
-    def unapply(props: Properties.T): Option[(String, String)] =
-      props match {
-        case List((FUNCTION, "command_decl"), (Markup.NAME, name), (Markup.KIND, kind)) =>
-          Some((name, kind))
-        case _ => None
-      }
-  }
-
   val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
   val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
 
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML	Tue Aug 07 22:32:14 2012 +0200
@@ -37,16 +37,15 @@
                   fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
                   fn ([], a) =>
                     let
-                      val ((((master, name), imports), keywords), uses) =
-                        pair (pair (pair (pair string string) (list string))
-                          (list (pair string (option (pair string (list string))))))
-                          (list (pair string bool)) a;
-                      val res =
-                        Exn.capture (fn () =>
-                          (master, Thy_Header.make name imports keywords
-                            (map (apfst Path.explode) uses))) ();
-                    in Document.Header res end,
-                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
+                      val (master, (name, (imports, (keywords, (uses, errors))))) =
+                        pair string (pair string (pair (list string)
+                          (pair (list (pair string (option (pair string (list string)))))
+                            (pair (list (pair string bool)) (list string))))) a;
+                      val (uses', errors') =
+                        (map (apfst Path.explode) uses, errors)
+                          handle ERROR msg => ([], errors @ [msg]);
+                      val header = Thy_Header.make name imports keywords uses';
+                    in Document.Deps (master, header, errors') end,
                   fn (a, []) => Document.Perspective (map int_atom a)]))
             end;
 
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -195,7 +195,7 @@
 
   def define_command(command: Command): Unit =
     input("Document.define_command",
-      Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
+      Document.ID(command.id), encode(command.name), encode(command.source))
 
 
   /* document versions */
@@ -210,30 +210,28 @@
     val edits_yxml =
     { import XML.Encode._
       def id: T[Command] = (cmd => long(cmd.id))
-      def symbol_string: T[String] = (s => string(Symbol.encode(s)))
       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(deps)) =>
+          { case Document.Node.Deps(header) =>
               val dir = Isabelle_System.posix_path(name.dir)
-              val imports = deps.imports.map(_.node)
+              val imports = header.imports.map(_.node)
               // FIXME val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
-              val uses = deps.uses
+              val uses = header.uses
               (Nil,
-                pair(pair(pair(pair(symbol_string, symbol_string), list(symbol_string)),
-                  list(pair(symbol_string, option(pair(symbol_string, list(symbol_string)))))),
-                    list(pair(symbol_string, bool)))(
-                (((dir, name.theory), imports), deps.keywords), uses)) },
-          { case Document.Node.Header(Exn.Exn(e)) => (List(Symbol.encode(Exn.message(e))), Nil) },
+                pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
+                  pair(list(pair(Encode.string, option(pair(Encode.string, list(Encode.string))))),
+                  pair(list(pair(Encode.string, bool)), list(Encode.string))))))(
+                (dir, (name.theory, (imports, (header.keywords, (uses, header.errors))))))) },
           { 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) =>
+      def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
       {
         val (name, edit) = node_edit
         pair(string, encode_edit(name))(name.node, edit)
       })
-      YXML.string_of_body(encode(edits)) }
+      YXML.string_of_body(encode_edits(edits)) }
     input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
   }
 
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Proof/extraction.ML	Tue Aug 07 22:32:14 2012 +0200
@@ -120,7 +120,7 @@
 fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
 fun corr_name s vs = extr_name s vs ^ "_correctness";
 
-fun msg d s = Output.urgent_message (Symbol.spaces d ^ s);
+fun msg d s = Output.urgent_message (Pretty.spaces d ^ s);
 
 fun vars_of t = map Var (rev (Term.add_vars t []));
 fun frees_of t = map Free (rev (Term.add_frees t []));
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/System/build.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -163,19 +163,19 @@
 
   /* parser */
 
+  private val SESSION = "session"
+  private val IN = "in"
+  private val DESCRIPTION = "description"
+  private val OPTIONS = "options"
+  private val THEORIES = "theories"
+  private val FILES = "files"
+
+  lazy val root_syntax =
+    Outer_Syntax.init() + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
+      (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
+
   private object Parser extends Parse.Parser
   {
-    val SESSION = "session"
-    val IN = "in"
-    val DESCRIPTION = "description"
-    val OPTIONS = "options"
-    val THEORIES = "theories"
-    val FILES = "files"
-
-    val syntax =
-      Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
-        SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
-
     def session_entry(pos: Position.T): Parser[Session_Entry] =
     {
       val session_name = atom("session name", _.is_name)
@@ -188,7 +188,7 @@
         keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
           { case _ ~ (x ~ y) => (x, y) }
 
-      ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
+      ((command(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
         (keyword("!") ^^^ true | success(false)) ~
         (keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~
         (opt(keyword(IN) ~! path ^^ { case _ ~ x => x })) ~
@@ -202,7 +202,7 @@
 
     def parse_entries(root: Path): List[Session_Entry] =
     {
-      val toks = syntax.scan(File.read(root))
+      val toks = root_syntax.scan(File.read(root))
       parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)
@@ -315,22 +315,22 @@
   }
 
 
-  /* source dependencies */
+  /* source dependencies and static content */
 
-  sealed case class Node(
+  sealed case class Session_Content(
     loaded_theories: Set[String],
     syntax: Outer_Syntax,
     sources: List[(Path, SHA1.Digest)])
 
-  sealed case class Deps(deps: Map[String, Node])
+  sealed case class Deps(deps: Map[String, Session_Content])
   {
     def is_empty: Boolean = deps.isEmpty
-    def apply(name: String): Node = deps(name)
+    def apply(name: String): Session_Content = deps(name)
     def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   }
 
   def dependencies(verbose: Boolean, tree: Session_Tree): Deps =
-    Deps((Map.empty[String, Node] /: tree.topological_order)(
+    Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
       { case (deps, (name, info)) =>
           val (preloaded, parent_syntax) =
             info.parent match {
@@ -358,19 +358,12 @@
                 map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
 
           val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
-
-          val keywords = thy_deps.map({ case (_, Exn.Res(h)) => h.keywords case _ => Nil }).flatten
-          val syntax = (parent_syntax /: keywords)(_ + _)
+          val syntax = (parent_syntax /: thy_deps) { case (syn, (_, h)) => syn.add_keywords(h) }
 
           val all_files =
             thy_deps.map({ case (n, h) =>
               val thy = Path.explode(n.node).expand
-              val uses =
-                h match {
-                  case Exn.Res(d) =>
-                    d.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
-                  case _ => Nil
-                }
+              val uses = h.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
               thy :: uses
             }).flatten ::: info.files.map(file => info.dir + file)
           val sources =
@@ -381,9 +374,17 @@
                   quote(name) + Position.str_of(info.pos))
             }
 
-          deps + (name -> Node(loaded_theories, syntax, sources))
+          deps + (name -> Session_Content(loaded_theories, syntax, sources))
       }))
 
+  def session_content(session: String): Session_Content =
+  {
+    val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session))
+    dependencies(false, tree)(session)
+  }
+
+  def outer_syntax(session: String): Outer_Syntax = session_content(session).syntax
+
 
   /* jobs */
 
@@ -398,7 +399,7 @@
         browser_info + Path.explode("isabelle.gif"))
       File.write(browser_info + Path.explode("index.html"),
         File.read(Path.explode("~~/lib/html/library_index_header.template")) +
-        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
+        File.read(Path.explode("~~/lib/html/library_index_Session_Content.template")) +
         File.read(Path.explode("~~/lib/html/library_index_footer.template")))
     }
 
@@ -702,15 +703,5 @@
       }
     }
   }
-
-
-  /* static outer syntax */
-
-  // FIXME Symbol.decode!?
-  def outer_syntax(session: String): Outer_Syntax =
-  {
-    val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session))
-    dependencies(false, tree)(session).syntax
-  }
 }
 
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Aug 07 22:32:14 2012 +0200
@@ -2,17 +2,15 @@
     Author:     Makarius
 
 Isabelle process wrapper, based on private fifos for maximum
-robustness and performance.
+robustness and performance, or local socket for maximum portability.
 
 Startup phases:
-  . raw Posix process startup with uncontrolled output on stdout/stderr
-  . stderr \002: ML running
-  .. stdin/stdout/stderr freely available (raw ML loop)
-  .. protocol thread initialization
-  ... rendezvous on system channel
-  ... message INIT(pid): channels ready
-  ... message RAW(keywords)
-  ... message RAW(ready): main loop ready
+  - raw Posix process startup with uncontrolled output on stdout/stderr
+  - stderr \002: ML running
+  - stdin/stdout/stderr freely available (raw ML loop)
+  - protocol thread initialization
+  - rendezvous on system channel
+  - message INIT: channels ready
 *)
 
 signature ISABELLE_PROCESS =
@@ -96,7 +94,7 @@
 
 in
 
-fun setup_channels channel =
+fun init_channels channel =
   let
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF);
     val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF);
@@ -178,15 +176,10 @@
       Unsynchronized.change print_mode
         (fn mode =>
           (mode @ [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN])
-          |> fold (update op =)
-            [Symbol.xsymbolsN, isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
+          |> fold (update op =) [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]);
 
     val channel = rendezvous ();
-    val _ = setup_channels channel;
-
-    val _ = Keyword.status ();
-    val _ = Thy_Info.status ();
-    val _ = Output.protocol_message Isabelle_Markup.ready "";
+    val _ = init_channels channel;
   in loop channel end));
 
 fun init_fifos fifo1 fifo2 = init (fn () => System_Channel.fifo_rendezvous fifo1 fifo2);
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -83,6 +83,17 @@
   import Isabelle_Process._
 
 
+  /* text representation */
+
+  def encode(s: String): String = Symbol.encode(s)
+  def decode(s: String): String = Symbol.decode(s)
+
+  object Encode
+  {
+    val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
+  }
+
+
   /* output */
 
   private def system_output(text: String)
@@ -264,7 +275,7 @@
             else done = true
           }
           if (result.length > 0) {
-            output_message(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
+            output_message(markup, Nil, List(XML.Text(decode(result.toString))))
             result.length = 0
           }
           else {
@@ -323,7 +334,7 @@
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
-      def read_chunk(decode: Boolean): XML.Body =
+      def read_chunk(do_decode: Boolean): XML.Body =
       {
         //{{{
         // chunk size
@@ -350,8 +361,8 @@
 
         if (i != n) throw new Protocol_Error("bad message chunk content")
 
-        if (decode)
-          YXML.parse_body_failsafe(Standard_System.decode_chars(Symbol.decode, buf, 0, n))
+        if (do_decode)
+          YXML.parse_body_failsafe(Standard_System.decode_chars(decode, buf, 0, n))
         else List(XML.Text(Standard_System.decode_chars(s => s, buf, 0, n).toString))
         //}}}
       }
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/System/options.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -30,13 +30,15 @@
 
   /* parsing */
 
+  private val DECLARE = "declare"
+  private val DEFINE = "define"
+
+  lazy val options_syntax =
+    Outer_Syntax.init() + ":" + "=" + "--" +
+      (DECLARE, Keyword.THY_DECL) + (DEFINE, Keyword.PRF_DECL)
+
   private object Parser extends Parse.Parser
   {
-    val DECLARE = "declare"
-    val DEFINE = "define"
-
-    val syntax = Outer_Syntax.empty + ":" + "=" + "--" + DECLARE + DEFINE
-
     val entry: Parser[Options => Options] =
     {
       val option_name = atom("option name", _.is_xname)
@@ -47,16 +49,17 @@
           { case s ~ n => if (s.isDefined) "-" + n else n } |
         atom("option value", tok => tok.is_name || tok.is_float)
 
-      keyword(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~
+      command(DECLARE) ~! (option_name ~ keyword(":") ~ option_type ~
       keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
         { case _ ~ (a ~ _ ~ b ~ _ ~ c ~ d) => (options: Options) => options.declare(a, b, c, d) } |
-      keyword(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^
+      command(DEFINE) ~! (option_name ~ keyword("=") ~ option_value) ^^
         { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) }
     }
 
     def parse_entries(file: Path): List[Options => Options] =
     {
-      parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.implode)) match {
+      val toks = options_syntax.scan(File.read(file))
+      parse_all(rep(entry), Token.reader(toks, file.implode)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)
       }
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/System/session.ML	Tue Aug 07 22:32:14 2012 +0200
@@ -71,6 +71,7 @@
 fun finish () =
   (Thy_Info.finish ();
     Present.finish ();
+    Keyword.status ();
     Outer_Syntax.check_syntax ();
     Future.shutdown ();
     Options.reset_default ();
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/System/session.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -37,7 +37,7 @@
 }
 
 
-class Session(thy_load: Thy_Load = new Thy_Load())
+class Session(val thy_load: Thy_Load = new Thy_Load())
 {
   /* global flags */
 
@@ -108,7 +108,7 @@
           val prev = previous.get_finished
           val (doc_edits, version) =
             Timing.timeit("Thy_Syntax.text_edits", timing) {
-              Thy_Syntax.text_edits(prover_syntax, prev, text_edits)
+              Thy_Syntax.text_edits(base_syntax, prev, text_edits)
             }
           version_result.fulfill(version)
           sender ! Change(doc_edits, prev, version)
@@ -125,11 +125,7 @@
 
   /* global state */
 
-  @volatile private var prover_syntax =
-    Outer_Syntax.init() +
-      // FIXME avoid hardwired stuff!?
-      ("hence", Keyword.PRF_ASM_GOAL, "then have") +
-      ("thus", Keyword.PRF_ASM_GOAL, "then show")
+  @volatile private var base_syntax = Outer_Syntax.init()
 
   private val syslog = Volatile(Queue.empty[XML.Elem])
   def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
@@ -149,9 +145,12 @@
   def recent_syntax(): Outer_Syntax =
   {
     val version = current_state().recent_finished.version.get_finished
-    if (version.is_init) prover_syntax
+    if (version.is_init) base_syntax
     else version.syntax
   }
+  def get_recent_syntax(): Option[Outer_Syntax] =
+    if (is_ready) Some(recent_syntax)
+    else None
 
   def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
       pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
@@ -160,21 +159,19 @@
 
   /* theory files */
 
-  def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text =
+  def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
   {
-    val header1: Document.Node_Header =
-      header match {
-        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))
+    val header1 =
+      if (thy_load.is_loaded(name.theory))
+        header.error("Attempt to update loaded theory " + quote(name.theory))
+      else header
+    (name, Document.Node.Deps(header1))
   }
 
 
   /* actor messages */
 
-  private case class Start(args: List[String])
+  private case class Start(logic: String, args: List[String])
   private case object Cancel_Execution
   private case class Edit(edits: List[Document.Edit_Text])
   private case class Change(
@@ -357,25 +354,16 @@
         case Isabelle_Markup.Cancel_Scala(id) if output.is_protocol =>
           System.err.println("cancel_scala " + id)  // FIXME actually cancel JVM task
 
-        case Isabelle_Markup.Ready if output.is_protocol =>
+        case _ if output.is_init =>
             phase = Session.Ready
 
-        case Isabelle_Markup.Loaded_Theory(name) if output.is_protocol =>
-          thy_load.register_thy(name)
-
-        case Isabelle_Markup.Command_Decl(name, kind) if output.is_protocol =>
-          prover_syntax += (name, kind)
-
-        case Isabelle_Markup.Keyword_Decl(name) if output.is_protocol =>
-          prover_syntax += name
-
         case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
           if (rc == 0) phase = Session.Inactive
           else phase = Session.Failed
 
-        case _ =>
-          if (output.is_init || output.is_stdout) { }
-          else bad_output(output)
+        case _ if output.is_stdout =>
+
+        case _ => bad_output(output)
       }
     }
     //}}}
@@ -389,9 +377,15 @@
       receiveWithin(delay_commands_changed.flush_timeout) {
         case TIMEOUT => delay_commands_changed.flush()
 
-        case Start(args) if prover.isEmpty =>
+        case Start(name, args) if prover.isEmpty =>
           if (phase == Session.Inactive || phase == Session.Failed) {
             phase = Session.Startup
+
+            // FIXME static init in main constructor
+            val content = Build.session_content(name)
+            thy_load.register_thys(content.loaded_theories)
+            base_syntax = content.syntax
+
             prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
           }
 
@@ -446,7 +440,7 @@
 
   /* actions */
 
-  def start(args: List[String]) { session_actor ! Start(args) }
+  def start(name: String, args: List[String]) { session_actor ! Start(name, args) }
 
   def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
 
@@ -456,7 +450,7 @@
   { session_actor !? Edit(edits) }
 
   def init_node(name: Document.Node.Name,
-    header: Document.Node_Header, perspective: Text.Perspective, text: String)
+    header: Document.Node.Header, perspective: Text.Perspective, text: String)
   {
     edit(List(header_edit(name, header),
       name -> Document.Node.Clear(),    // FIXME diff wrt. existing node
@@ -465,7 +459,7 @@
   }
 
   def edit_node(name: Document.Node.Name,
-    header: Document.Node_Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
+    header: Document.Node.Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
   {
     edit(List(header_edit(name, header),
       name -> Document.Node.Edits(text_edits),
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Thy/thy_header.ML	Tue Aug 07 22:32:14 2012 +0200
@@ -7,7 +7,8 @@
 signature THY_HEADER =
 sig
   type header =
-   {name: string, imports: string list,
+   {name: string,
+    imports: string list,
     keywords: (string * Keyword.spec option) list,
     uses: (Path.T * bool) list}
   val make: string -> string list -> (string * Keyword.spec option) list ->
@@ -23,7 +24,8 @@
 struct
 
 type header =
- {name: string, imports: string list,
+ {name: string,
+  imports: string list,
   keywords: (string * Keyword.spec option) list,
   uses: (Path.T * bool) list};
 
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Thy/thy_header.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -107,12 +107,17 @@
     try { read(reader).map(Standard_System.decode_permissive_utf8) }
     finally { reader.close }
   }
+
+
+  /* keywords */
+
+  type Keywords = List[(String, Option[(String, List[String])])]
 }
 
 
 sealed case class Thy_Header(
   name: String, imports: List[String],
-  keywords: List[Outer_Syntax.Decl],
+  keywords: Thy_Header.Keywords,
   uses: List[(String, Boolean)])
 {
   def map(f: String => String): Thy_Header =
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Aug 07 22:32:14 2012 +0200
@@ -10,7 +10,6 @@
   datatype action = Update | Remove
   val add_hook: (action -> string -> unit) -> unit
   val get_names: unit -> string list
-  val status: unit -> unit
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
   val is_finished: string -> bool
@@ -88,10 +87,6 @@
 
 fun get_names () = Graph.topological_order (get_thys ());
 
-fun status () =
-  List.app (fn name => Output.protocol_message (Isabelle_Markup.loaded_theory name) "")
-    (get_names ());
-
 
 (* access thy *)
 
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Thy/thy_info.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -24,7 +24,7 @@
 
   /* dependencies */
 
-  type Dep = (Document.Node.Name, Document.Node_Header)
+  type Dep = (Document.Node.Name, Document.Node.Header)
   private type Required = (List[Dep], Set[Document.Node.Name])
 
   private def require_thys(initiators: List[Document.Node.Name],
@@ -40,7 +40,7 @@
     else {
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
-        val node_deps =
+        val header =
           try { thy_load.check_thy(name) }
           catch {
             case ERROR(msg) =>
@@ -48,10 +48,13 @@
                 quote(name.theory) + required_by(initiators))
           }
         val (deps1, seen1) =
-          require_thys(name :: initiators, (deps, seen + name), node_deps.imports)
-        ((name, Exn.Res(node_deps)) :: deps1, seen1)
+          require_thys(name :: initiators, (deps, seen + name), header.imports)
+        ((name, header) :: deps1, seen1)
       }
-      catch { case e: Throwable => (((name, Exn.Exn(e)): Dep) :: deps, seen + name) }
+      catch {
+        case e: Throwable =>
+          ((name, Document.Node.bad_header(Exn.message(e))) :: deps, seen + name)
+      }
     }
   }
 
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -26,8 +26,11 @@
 
   private var loaded_theories: Set[String] = preloaded
 
-  def register_thy(thy_name: String): Unit =
-    synchronized { loaded_theories += thy_name }
+  def register_thy(name: String): Unit =
+    synchronized { loaded_theories += name }
+
+  def register_thys(names: Set[String]): Unit =
+    synchronized { loaded_theories ++= names }
 
   def is_loaded(thy_name: String): Boolean =
     synchronized { loaded_theories.contains(thy_name) }
@@ -36,7 +39,7 @@
   /* file-system operations */
 
   def append(dir: String, source_path: Path): String =
-    (Path.explode(dir) + source_path).implode
+    (Path.explode(dir) + source_path).expand.implode
 
   def read_header(name: Document.Node.Name): Thy_Header =
   {
@@ -60,7 +63,7 @@
     }
   }
 
-  def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Deps =
+  def check_header(name: Document.Node.Name, header: Thy_Header): Document.Node.Header =
   {
     val name1 = header.name
     val imports = header.imports.map(import_name(name.dir, _))
@@ -69,10 +72,10 @@
     if (name.theory != name1)
       error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
         " for theory " + quote(name1))
-    Document.Node.Deps(imports, header.keywords, uses)
+    Document.Node.Header(imports, header.keywords, uses)
   }
 
-  def check_thy(name: Document.Node.Name): Document.Node.Deps =
+  def check_thy(name: Document.Node.Name): Document.Node.Header =
     check_header(name, read_header(name))
 }
 
diff -r 1d2a12bb0640 -r 9775c2957000 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -33,7 +33,7 @@
 
       def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
       var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
-        List((0, "theory " + node_name.theory, buffer()))
+        List((0, node_name.theory, buffer()))
 
       @tailrec def close(level: Int => Boolean)
       {
@@ -134,26 +134,23 @@
     val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
 
     edits foreach {
-      case (name, Document.Node.Header(header)) =>
+      case (name, Document.Node.Deps(header)) =>
         val node = nodes(name)
         val update_header =
-          (node.header, header) match {
-            case (Exn.Res(deps0), Exn.Res(deps)) => deps0 != deps
-            case _ => true
-          }
+          !node.header.errors.isEmpty || !header.errors.isEmpty || node.header != header
         if (update_header) {
           val node1 = node.update_header(header)
-          updated_imports = updated_imports || (node.imports != node1.imports)
-          updated_keywords = updated_keywords || (node.keywords != node1.keywords)
+          updated_imports = updated_imports || (node.header.imports != node1.header.imports)
+          updated_keywords = updated_keywords || (node.header.keywords != node1.header.keywords)
           nodes += (name -> node1)
-          doc_edits += (name -> Document.Node.Header(header))
+          doc_edits += (name -> Document.Node.Deps(header))
         }
       case _ =>
     }
 
     val syntax =
       if (previous.is_init || updated_keywords)
-        (base_syntax /: nodes.entries)({ case (syn, (_, node)) => (syn /: node.keywords)(_ + _) })
+        (base_syntax /: nodes.entries) { case (syn, (_, node)) => syn.add_keywords(node.header) }
       else previous.syntax
 
     val reparse =
@@ -289,7 +286,7 @@
         doc_edits += (name -> Document.Node.Edits(cmd_edits))
         nodes += (name -> node.update_commands(commands3))
 
-      case (name, Document.Node.Header(_)) =>
+      case (name, Document.Node.Deps(_)) =>
 
       case (name, Document.Node.Perspective(text_perspective)) =>
         val node = nodes(name)
diff -r 1d2a12bb0640 -r 9775c2957000 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props	Tue Aug 07 22:32:14 2012 +0200
@@ -67,9 +67,16 @@
 isabelle-syslog.title=Syslog
 
 #SideKick
-sidekick.parser.isabelle.label=Isabelle
+mode.isabelle-options.folding=sidekick
+mode.isabelle-options.sidekick.parser=isabelle-options
+mode.isabelle-root.folding=sidekick
+mode.isabelle-root.sidekick.parser=isabelle-root
+mode.isabelle.customSettings=true
+mode.isabelle.folding=sidekick
 mode.isabelle.sidekick.parser=isabelle
+mode.isabelle.sidekick.showStatusWindow.label=true
 mode.ml.sidekick.parser=isabelle
+sidekick.parser.isabelle.label=Isabelle
 
 #Hyperlinks
 mode.isabelle.hyperlink.source=isabelle
diff -r 1d2a12bb0640 -r 9775c2957000 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -63,13 +63,16 @@
 {
   /* header */
 
-  def node_header(): Document.Node_Header =
+  def node_header(): Document.Node.Header =
   {
     Swing_Thread.require()
     Isabelle.buffer_lock(buffer) {
       Exn.capture {
         Isabelle.thy_load.check_header(name,
           Thy_Header.read(buffer.getSegment(0, buffer.getLength)))
+      } match {
+        case Exn.Res(header) => header
+        case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
       }
     }
   }
diff -r 1d2a12bb0640 -r 9775c2957000 src/Tools/jEdit/src/html_panel.scala
--- a/src/Tools/jEdit/src/html_panel.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/html_panel.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -134,7 +134,7 @@
       val (font_metrics, margin) =
         Swing_Thread.now {
           val metrics = getFontMetrics(font)
-          (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20)
+          (metrics, (getWidth() / (metrics.charWidth(Pretty.spc) max 1) - 4) max 20)
         }
       if (current_font_metrics == null ||
           current_font_family != font_family ||
diff -r 1d2a12bb0640 -r 9775c2957000 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -48,14 +48,15 @@
 }
 
 
-abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)
+class Isabelle_Sidekick(name: String, get_syntax: => Option[Outer_Syntax])
+  extends SideKickParser(name)
 {
   /* parsing */
 
   @volatile protected var stopped = false
   override def stop() = { stopped = true }
 
-  def parser(data: SideKickParsedData, model: Document_Model): Unit
+  def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
 
   def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
   {
@@ -66,12 +67,16 @@
     val root = data.root
     data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
 
-    Swing_Thread.now { Document_Model(buffer) } match {
-      case Some(model) =>
-        parser(data, model)
-        if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
-      case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
-    }
+    val syntax = get_syntax
+    val ok =
+      if (syntax.isDefined) {
+        val ok = parser(buffer, syntax.get, data)
+        if (stopped) { root.add(new DefaultMutableTreeNode("<stopped>")); true }
+        else ok
+      }
+      else false
+    if (!ok) root.add(new DefaultMutableTreeNode("<ignored>"))
+
     data
   }
 
@@ -87,15 +92,14 @@
 
     val buffer = pane.getBuffer
     Isabelle.buffer_lock(buffer) {
-      Document_Model(buffer) match {
+      get_syntax match {
         case None => null
-        case Some(model) =>
+        case Some(syntax) =>
           val line = buffer.getLineOfOffset(caret)
           val start = buffer.getLineStartOffset(line)
           val text = buffer.getSegment(start, caret - start)
 
-          val completion = model.session.recent_syntax().completion
-          completion.complete(text) match {
+          syntax.completion.complete(text) match {
             case None => null
             case Some((word, cs)) =>
               val ds =
@@ -128,14 +132,16 @@
 }
 
 
-class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
+class Isabelle_Sidekick_Structure(
+    name: String,
+    get_syntax: => Option[Outer_Syntax],
+    node_name: Buffer => Option[Document.Node.Name])
+  extends Isabelle_Sidekick(name, get_syntax)
 {
   import Thy_Syntax.Structure
 
-  def parser(data: SideKickParsedData, model: Document_Model)
+  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   {
-    val syntax = model.session.recent_syntax()
-
     def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
       entry match {
         case Structure.Block(name, body) =>
@@ -157,36 +163,57 @@
         case _ => Nil
       }
 
-    val text = Isabelle.buffer_text(model.buffer)
-    val structure = Structure.parse(syntax, model.name, text)
-
-    make_tree(0, structure) foreach (node => data.root.add(node))
+    node_name(buffer) match {
+      case Some(name) =>
+        val text = Isabelle.buffer_text(buffer)
+        val structure = Structure.parse(syntax, name, text)
+        make_tree(0, structure) foreach (node => data.root.add(node))
+        true
+      case None => false
+    }
   }
 }
 
 
-class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
+class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
+  "isabelle", Isabelle.session.get_recent_syntax, Isabelle.buffer_node_name)
+
+
+class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
+  "isabelle-options", Some(Options.options_syntax), Isabelle.buffer_node_dummy)
+
+
+class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure(
+  "isabelle-root", Some(Build.root_syntax), Isabelle.buffer_node_dummy)
+
+
+class Isabelle_Sidekick_Raw
+  extends Isabelle_Sidekick("isabelle-raw", Isabelle.session.get_recent_syntax)
 {
-  def parser(data: SideKickParsedData, model: Document_Model)
+  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   {
-    val root = data.root
-    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
-    for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
-      snapshot.state.command_state(snapshot.version, command).markup
-        .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
-          {
-            val range = info.range + command_start
-            val content = command.source(info.range).replace('\n', ' ')
-            val info_text =
-              Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
+    Swing_Thread.now { Document_Model(buffer).map(_.snapshot) } match {
+      case Some(snapshot) =>
+        val root = data.root
+        for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
+          snapshot.state.command_state(snapshot.version, command).markup
+            .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
+              {
+                val range = info.range + command_start
+                val content = command.source(info.range).replace('\n', ' ')
+                val info_text =
+                  Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
 
-            new DefaultMutableTreeNode(
-              new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
-                override def getShortString: String = content
-                override def getLongString: String = info_text
-                override def toString = quote(content) + " " + range.toString
+                new DefaultMutableTreeNode(
+                  new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
+                    override def getShortString: String = content
+                    override def getLongString: String = info_text
+                    override def toString = quote(content) + " " + range.toString
+                  })
               })
-          })
+        }
+        true
+      case None => false
     }
   }
 }
diff -r 1d2a12bb0640 -r 9775c2957000 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Tue Aug 07 22:32:14 2012 +0200
@@ -180,14 +180,11 @@
 isabelle-output.dock-position=bottom
 isabelle-output.height=174
 isabelle-output.width=412
+isabelle-readme.dock-position=bottom
 isabelle-session.dock-position=bottom
-isabelle-readme.dock-position=bottom
 line-end.shortcut=END
 line-home.shortcut=HOME
 lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
-mode.isabelle.customSettings=true
-mode.isabelle.folding=sidekick
-mode.isabelle.sidekick.showStatusWindow.label=true
 print.font=IsabelleText
 restore.remote=false
 restore=false
diff -r 1d2a12bb0640 -r 9775c2957000 src/Tools/jEdit/src/modes/isabelle-options.xml
--- a/src/Tools/jEdit/src/modes/isabelle-options.xml	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-options.xml	Tue Aug 07 22:32:14 2012 +0200
@@ -4,34 +4,10 @@
 <!-- Isabelle options mode -->
 <MODE>
   <PROPS>
-    <PROPERTY NAME="commentStart" VALUE="(*"/>
-    <PROPERTY NAME="commentEnd" VALUE="*)"/>
     <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
     <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
     <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
     <PROPERTY NAME="tabSize" VALUE="2" />
     <PROPERTY NAME="indentSize" VALUE="2" />
   </PROPS>
-  <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
-    <SPAN TYPE="COMMENT1">
-      <BEGIN>(*</BEGIN>
-      <END>*)</END>
-    </SPAN>
-    <SPAN TYPE="COMMENT3">
-      <BEGIN>{*</BEGIN>
-      <END>*}</END>
-    </SPAN>
-    <SPAN TYPE="LITERAL2">
-      <BEGIN>`</BEGIN>
-      <END>`</END>
-    </SPAN>
-    <SPAN TYPE="LITERAL1">
-      <BEGIN>"</BEGIN>
-      <END>"</END>
-    </SPAN>
-    <KEYWORDS>
-      <KEYWORD1>declare</KEYWORD1>
-      <KEYWORD2>define</KEYWORD2>
-    </KEYWORDS>
-  </RULES>
 </MODE>
diff -r 1d2a12bb0640 -r 9775c2957000 src/Tools/jEdit/src/modes/isabelle-root.xml
--- a/src/Tools/jEdit/src/modes/isabelle-root.xml	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/modes/isabelle-root.xml	Tue Aug 07 22:32:14 2012 +0200
@@ -4,38 +4,10 @@
 <!-- Isabelle session root mode -->
 <MODE>
   <PROPS>
-    <PROPERTY NAME="commentStart" VALUE="(*"/>
-    <PROPERTY NAME="commentEnd" VALUE="*)"/>
     <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
     <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
     <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
     <PROPERTY NAME="tabSize" VALUE="2" />
     <PROPERTY NAME="indentSize" VALUE="2" />
   </PROPS>
-  <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
-    <SPAN TYPE="COMMENT1">
-      <BEGIN>(*</BEGIN>
-      <END>*)</END>
-    </SPAN>
-    <SPAN TYPE="COMMENT3">
-      <BEGIN>{*</BEGIN>
-      <END>*}</END>
-    </SPAN>
-    <SPAN TYPE="LITERAL2">
-      <BEGIN>`</BEGIN>
-      <END>`</END>
-    </SPAN>
-    <SPAN TYPE="LITERAL1">
-      <BEGIN>"</BEGIN>
-      <END>"</END>
-    </SPAN>
-    <KEYWORDS>
-      <KEYWORD1>session</KEYWORD1>
-      <KEYWORD2>in</KEYWORD2>
-      <KEYWORD2>description</KEYWORD2>
-      <KEYWORD2>files</KEYWORD2>
-      <KEYWORD2>options</KEYWORD2>
-      <KEYWORD2>theories</KEYWORD2>
-    </KEYWORDS>
-  </RULES>
 </MODE>
diff -r 1d2a12bb0640 -r 9775c2957000 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -147,6 +147,15 @@
 
   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
 
+  def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
+    Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
+
+  def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
+  {
+    val name = buffer_name(buffer)
+    Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
+  }
+
 
   /* main jEdit components */
 
@@ -197,18 +206,14 @@
   {
     swing_buffer_lock(buffer) {
       val opt_model =
-      {
-        val name = buffer_name(buffer)
-        Thy_Header.thy_name(name) match {
-          case Some(theory) =>
-            val node_name = Document.Node.Name(name, buffer.getDirectory, theory)
+        buffer_node_name(buffer) match {
+          case Some(node_name) =>
             document_model(buffer) match {
               case Some(model) if model.name == node_name => Some(model)
               case _ => Some(Document_Model.init(session, buffer, node_name))
             }
           case None => None
         }
-      }
       if (opt_model.isDefined) {
         for (text_area <- jedit_text_areas(buffer)) {
           if (document_view(text_area).map(_.model) != opt_model)
@@ -301,7 +306,8 @@
       if (logic != null && logic != "") logic
       else Isabelle.default_logic()
     }
-    session.start(modes ::: List(logic))
+    val name = Path.explode(logic).base.implode  // FIXME more robust session name
+    session.start(name, modes ::: List(logic))
   }
 
 
diff -r 1d2a12bb0640 -r 9775c2957000 src/Tools/jEdit/src/services.xml
--- a/src/Tools/jEdit/src/services.xml	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/services.xml	Tue Aug 07 22:32:14 2012 +0200
@@ -8,6 +8,12 @@
 	<SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
 		new isabelle.jedit.Isabelle_Sidekick_Default();
 	</SERVICE>
+	<SERVICE NAME="isabelle-options" CLASS="sidekick.SideKickParser">
+		new isabelle.jedit.Isabelle_Sidekick_Options();
+	</SERVICE>
+	<SERVICE NAME="isabelle-root" CLASS="sidekick.SideKickParser">
+		new isabelle.jedit.Isabelle_Sidekick_Root();
+	</SERVICE>
 	<SERVICE NAME="isabelle-raw" CLASS="sidekick.SideKickParser">
 		new isabelle.jedit.Isabelle_Sidekick_Raw();
 	</SERVICE>
diff -r 1d2a12bb0640 -r 9775c2957000 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Tue Aug 07 14:29:18 2012 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Aug 07 22:32:14 2012 +0200
@@ -162,7 +162,7 @@
       }
   }
 
-  class Marker extends TokenMarker
+  class Marker(ext_styles: Boolean, get_syntax: => Option[Outer_Syntax]) extends TokenMarker
   {
     override def markTokens(context: TokenMarker.LineContext,
         handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
@@ -176,12 +176,12 @@
 
       val context1 =
       {
+        val syntax = get_syntax
         val (styled_tokens, context1) =
-          if (line_ctxt.isDefined && Isabelle.session.is_ready) {
-            val syntax = Isabelle.session.recent_syntax()
-            val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
+          if (line_ctxt.isDefined && syntax.isDefined) {
+            val (tokens, ctxt1) = syntax.get.scan_context(line, line_ctxt.get)
             val styled_tokens =
-              tokens.map(tok => (Isabelle_Rendering.token_markup(syntax, tok), tok))
+              tokens.map(tok => (Isabelle_Rendering.token_markup(syntax.get, tok), tok))
             (styled_tokens, new Line_Context(Some(ctxt1)))
           }
           else {
@@ -189,7 +189,9 @@
             (List((JEditToken.NULL, token)), new Line_Context(None))
           }
 
-        val extended = extended_styles(line)
+        val extended =
+          if (ext_styles) extended_styles(line)
+          else Map.empty[Text.Offset, Byte => Byte]
 
         var offset = 0
         for ((style, token) <- styled_tokens) {
@@ -221,7 +223,10 @@
 
   /* mode provider */
 
-  private val isabelle_token_marker = new Token_Markup.Marker
+  private val markers = Map(
+    "isabelle" -> new Token_Markup.Marker(true, Isabelle.session.get_recent_syntax()),
+    "isabelle-options" -> new Token_Markup.Marker(false, Some(Options.options_syntax)),
+    "isabelle-root" -> new Token_Markup.Marker(false, Some(Build.root_syntax)))
 
   class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
   {
@@ -230,15 +235,14 @@
     override def loadMode(mode: Mode, xmh: XModeHandler)
     {
       super.loadMode(mode, xmh)
-      if (mode.getName == "isabelle")
-        mode.setTokenMarker(isabelle_token_marker)
+      markers.get(mode.getName).map(mode.setTokenMarker(_))
     }
   }
 
   def refresh_buffer(buffer: JEditBuffer)
   {
     buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
-    buffer.setTokenMarker(isabelle_token_marker)
+    markers.get(buffer.getMode.getName).map(buffer.setTokenMarker(_))
   }
 }