merged
authorwenzelm
Tue, 08 Apr 2014 23:16:00 +0200
changeset 56478 92345da2349f
parent 56456 39281b3e4fac (current diff)
parent 56477 57b5c8db55f1 (diff)
child 56479 91958d4b30f7
merged
--- a/src/Doc/JEdit/JEdit.thy	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Tue Apr 08 23:16:00 2014 +0200
@@ -564,13 +564,6 @@
   determines an additional delay (0.0 by default), before opening a
   completion popup.
 
-  \item The system option @{system_option
-  jedit_completion_dismiss_delay} determines an additional delay (0.0
-  by default), before dismissing an earlier completion popup.  A value
-  like 0.1 is occasionally useful to reduce the chance of loosing key
-  strokes when the speed of typing exceeds that of repainting GUI
-  components.
-
   \item The system option @{system_option jedit_completion_immediate}
   (disabled by default) controls whether replacement text should be
   inserted immediately without popup.  This is restricted to Isabelle
--- a/src/Doc/antiquote_setup.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Doc/antiquote_setup.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -201,6 +201,10 @@
       val _ = Context_Position.reports ctxt (map (pair pos) markup);
     in true end;
 
+fun check_system_option ctxt (name, pos) =
+  (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true)
+    handle ERROR _ => false;
+
 fun check_tool ctxt (name, pos) =
   let
     fun tool dir =
@@ -265,7 +269,7 @@
     entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #>
     entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #>
     entity_antiqs no_check "isatt" @{binding setting} #>
-    entity_antiqs no_check "isatt" @{binding system_option} #>
+    entity_antiqs check_system_option "isatt" @{binding system_option} #>
     entity_antiqs no_check "" @{binding inference} #>
     entity_antiqs no_check "isatt" @{binding executable} #>
     entity_antiqs check_tool "isatool" @{binding tool} #>
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -124,7 +124,7 @@
             | SOME _ => (GenuineCex, Quickcheck.timings_of result)
           end) ()
   handle TimeLimit.TimeOut =>
-         (Timeout, [("timelimit", Real.floor (Options.default_real @{option auto_time_limit}))])
+         (Timeout, [("timelimit", Real.floor (Options.default_real @{system_option auto_time_limit}))])
 
 fun quickcheck_mtd change_options quickcheck_generator =
   ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options)
--- a/src/HOL/Prolog/prolog.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/Prolog/prolog.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -2,7 +2,7 @@
     Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
 *)
 
-Options.default_put_bool @{option show_main_goal} true;
+Options.default_put_bool @{system_option show_main_goal} true;
 
 structure Prolog =
 struct
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -285,7 +285,7 @@
 
 type tptp_problem = tptp_line list
 
-fun debug f x = if Options.default_bool @{option ML_exception_trace} then (f x; ()) else ()
+fun debug f x = if Options.default_bool @{system_option ML_exception_trace} then (f x; ()) else ()
 
 fun nameof_tff_atom_type (Atom_type str) = str
   | nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Apr 08 23:16:00 2014 +0200
@@ -42,7 +42,7 @@
 ML {*
   if test_all @{context} then ()
   else
-    (Options.default_put_bool @{option ML_exception_trace} true;
+    (Options.default_put_bool @{system_option ML_exception_trace} true;
      default_print_depth 200;  (* FIXME proper ML_print_depth within context!? *)
      PolyML.Compiler.maxInlineSize := 0)
 *}
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -34,7 +34,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    @{option auto_nitpick}
+    @{system_option auto_nitpick}
     "auto-nitpick"
     "Run Nitpick automatically"
 
@@ -396,6 +396,6 @@
 
 fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
 
-val _ = Try.tool_setup (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
+val _ = Try.tool_setup (nitpickN, (50, @{system_option auto_nitpick}, try_nitpick))
 
 end;
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -100,7 +100,7 @@
 
 fun z3_non_commercial () =
   let
-    val flag1 = Options.default_string @{option z3_non_commercial}
+    val flag1 = Options.default_string @{system_option z3_non_commercial}
     val flag2 = getenv "Z3_NON_COMMERCIAL"
   in
     if accepted flag1 then Z3_Non_Commercial_Accepted
--- a/src/HOL/Tools/SMT2/smt2_systems.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/Tools/SMT2/smt2_systems.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -97,7 +97,7 @@
 
 fun z3_non_commercial () =
   let
-    val flag1 = Options.default_string @{option z3_non_commercial}
+    val flag1 = Options.default_string @{system_option z3_non_commercial}
     val flag2 = getenv "Z3_NON_COMMERCIAL"
   in
     if accepted flag1 then Z3_Non_Commercial_Accepted
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -43,7 +43,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    @{option auto_sledgehammer}
+    @{system_option auto_sledgehammer}
     "auto-sledgehammer"
     "Run Sledgehammer automatically"
 
@@ -72,7 +72,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_proof
     NONE
-    @{option sledgehammer_timeout}
+    @{system_option sledgehammer_timeout}
     "Sledgehammer: Time Limit"
     "ATPs will be interrupted after this time (in seconds)"
 
@@ -229,7 +229,7 @@
     |> fold (AList.default (op =))
          [("provers", [(case !provers of "" => default_provers_param_value mode ctxt | s => s)]),
           ("timeout",
-           let val timeout = Options.default_int @{option sledgehammer_timeout} in
+           let val timeout = Options.default_int @{system_option sledgehammer_timeout} in
              [if timeout <= 0 then "none" else string_of_int timeout]
            end)]
   end
@@ -472,7 +472,7 @@
       state
   end
 
-val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
+val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))
 
 val _ =
   Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
--- a/src/HOL/Tools/try0.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/HOL/Tools/try0.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -25,7 +25,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    @{option auto_methods}
+    @{system_option auto_methods}
     "auto-try0"
     "Try standard proof methods";
 
@@ -193,6 +193,6 @@
 
 fun try_try0 auto = generic_try0 (if auto then Auto_Try else Try) NONE ([], [], [], []);
 
-val _ = Try.tool_setup (try0N, (30, @{option auto_methods}, try_try0));
+val _ = Try.tool_setup (try0N, (30, @{system_option auto_methods}, try_try0));
 
 end;
--- a/src/Pure/General/position.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/General/position.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -35,6 +35,7 @@
   val default_properties: T -> Properties.T -> Properties.T
   val markup: T -> Markup.T -> Markup.T
   val is_reported: T -> bool
+  val is_reported_range: T -> bool
   val reported_text: T -> Markup.T -> string -> string
   val report_text: T -> Markup.T -> string -> unit
   val report: T -> Markup.T -> unit
@@ -166,6 +167,7 @@
 (* reports *)
 
 fun is_reported pos = is_some (offset_of pos) andalso is_some (get_id pos);
+fun is_reported_range pos = is_reported pos andalso is_some (end_offset_of pos);
 
 fun reported_text pos m txt = if is_reported pos then Markup.markup (markup pos m) txt else "";
 fun report_text pos markup txt = Output.report [reported_text pos markup txt];
--- a/src/Pure/General/position.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/General/position.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -30,6 +30,10 @@
 
   object Line_File
   {
+    def apply(line: Int, file: String): T =
+      (if (line > 0) Line(line) else Nil) :::
+      (if (file != "") File(file) else Nil)
+
     def unapply(pos: T): Option[(Int, String)] =
       (pos, pos) match {
         case (Line(i), File(name)) => Some((i, name))
@@ -79,10 +83,15 @@
 
   object Reported
   {
-    def unapply(pos: T): Option[(Long, String, Symbol.Range)] =
+    def unapply(pos: T): Option[(Long, Text.Chunk.Name, Symbol.Range)] =
       (pos, pos) match {
         case (Id(id), Range(range)) =>
-          Some((id, File.unapply(pos).getOrElse(""), range))
+          val chunk_name =
+            pos match {
+              case File(name) => Text.Chunk.File(name)
+              case _ => Text.Chunk.Default
+            }
+          Some((id, chunk_name, range))
         case _ => None
       }
   }
--- a/src/Pure/General/symbol.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/General/symbol.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -125,16 +125,14 @@
 
   object Index
   {
-    def apply(text: CharSequence): Index = new Index(text)
-  }
+    private sealed case class Entry(chr: Int, sym: Int)
 
-  final class Index private(text: CharSequence)
-  {
-    private sealed case class Entry(chr: Int, sym: Int)
-    private val index: Array[Entry] =
+    val empty: Index = new Index(Nil)
+
+    def apply(text: CharSequence): Index =
     {
       val matcher = new Matcher(text)
-      val buf = new mutable.ArrayBuffer[Entry]
+      val buf = new mutable.ListBuffer[Entry]
       var chr = 0
       var sym = 0
       while (chr < text.length) {
@@ -143,8 +141,14 @@
         sym += 1
         if (n > 1) buf += Entry(chr, sym)
       }
-      buf.toArray
+      if (buf.isEmpty) empty else new Index(buf.toList)
     }
+  }
+
+  final class Index private(entries: List[Index.Entry])
+  {
+    private val hash: Int = entries.hashCode
+    private val index: Array[Index.Entry] = entries.toArray
 
     def decode(symbol_offset: Offset): Text.Offset =
     {
@@ -166,7 +170,6 @@
     }
     def decode(symbol_range: Range): Text.Range = symbol_range.map(decode(_))
 
-    private val hash: Int = index.toList.hashCode
     override def hashCode: Int = hash
     override def equals(that: Any): Boolean =
       that match {
--- a/src/Pure/Isar/isar_syn.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -984,7 +984,7 @@
     (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
       Toplevel.keep (fn state =>
        (if Isabelle_Process.is_active () then error "Illegal TTY command" else ();
-        case limit of NONE => () | SOME n => Options.default_put_int @{option goals_limit} n;
+        case limit of NONE => () | SOME n => Options.default_put_int @{system_option goals_limit} n;
         Toplevel.quiet := false;
         Print_Mode.with_modes modes (Toplevel.print_state true) state))));
 
--- a/src/Pure/Isar/parse.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/Isar/parse.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -25,31 +25,37 @@
       if (!filter_proper || in.atEnd || in.first.is_proper) in
       else proper(in.rest)
 
-    def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
-    {
-      def apply(raw_input: Input) =
-      {
-        val in = proper(raw_input)
-        if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
-        else {
-          val token = in.first
-          if (pred(token)) Success(token, proper(in.rest))
-          else
-            token.text match {
-              case (txt, "") =>
-                Failure(s + " expected,\nbut " + txt + " was found", in)
-              case (txt1, txt2) =>
-                Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
-            }
+    def token(s: String, pred: Elem => Boolean): Parser[(Elem, Token.Pos)] =
+      new Parser[(Elem, Token.Pos)] {
+        def apply(raw_input: Input) =
+        {
+          val in = proper(raw_input)
+          if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
+          else {
+            val pos =
+              in.pos match {
+                case pos: Token.Pos => pos
+                case _ => Token.Pos.none
+              }
+            val token = in.first
+            if (pred(token)) Success((token, pos), proper(in.rest))
+            else
+              token.text match {
+                case (txt, "") =>
+                  Failure(s + " expected,\nbut " + txt + " was found", in)
+                case (txt1, txt2) =>
+                  Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
+              }
+          }
         }
       }
-    }
 
     def atom(s: String, pred: Elem => Boolean): Parser[String] =
-      token(s, pred) ^^ (_.content)
+      token(s, pred) ^^ { case (tok, _) => tok.content }
 
-    def command(name: String): Parser[String] =
-      atom("command " + quote(name), tok => tok.is_command && tok.source == name)
+    def command(name: String): Parser[Position.T] =
+      token("command " + quote(name), tok => tok.is_command && tok.source == name) ^^
+        { case (_, pos) => pos.position }
 
     def keyword(name: String): Parser[String] =
       atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
--- a/src/Pure/Isar/token.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/Isar/token.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -121,25 +121,31 @@
 
   /* token reader */
 
-  class Position(val line: Int, val file: String) extends scala.util.parsing.input.Position
+  object Pos
+  {
+    val none: Pos = new Pos(0, "")
+  }
+
+  final class Pos private[Token](val line: Int, val file: String)
+    extends scala.util.parsing.input.Position
   {
     def column = 0
     def lineContents = ""
-    override def toString =
-      if (file == "") ("line " + line.toString)
-      else ("line " + line.toString + " of " + quote(file))
 
-    def advance(token: Token): Position =
+    def advance(token: Token): Pos =
     {
       var n = 0
       for (c <- token.content if c == '\n') n += 1
-      if (n == 0) this else new Position(line + n, file)
+      if (n == 0) this else new Pos(line + n, file)
     }
+
+    def position: Position.T = Position.Line_File(line, file)
+    override def toString: String = Position.here(position)
   }
 
   abstract class Reader extends scala.util.parsing.input.Reader[Token]
 
-  private class Token_Reader(tokens: List[Token], val pos: Position) extends Reader
+  private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader
   {
     def first = tokens.head
     def rest = new Token_Reader(tokens.tail, pos.advance(first))
@@ -147,7 +153,7 @@
   }
 
   def reader(tokens: List[Token], file: String = ""): Reader =
-    new Token_Reader(tokens, new Position(1, file))
+    new Token_Reader(tokens, new Pos(1, file))
 }
 
 
--- a/src/Pure/ML/ml_antiquotations.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -8,9 +8,10 @@
 struct
 
 val _ = Theory.setup
- (ML_Antiquotation.value @{binding option} (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
-    (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
-     ML_Syntax.print_string name))) #>
+ (ML_Antiquotation.value @{binding system_option}
+    (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
+      (Context_Position.report ctxt pos (Options.default_markup (name, pos));
+        ML_Syntax.print_string name))) #>
 
   ML_Antiquotation.value @{binding theory}
     (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
--- a/src/Pure/ML/ml_lex.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/ML/ml_lex.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -325,8 +325,12 @@
 val read = gen_read false;
 
 fun read_source SML {delimited, text, pos} =
-  (Position.report pos ((if SML then Markup.language_SML else Markup.language_ML) delimited);
-   gen_read SML pos text);
+  let
+    val language = if SML then Markup.language_SML else Markup.language_ML;
+    val _ =
+      if Position.is_reported_range pos then Position.report pos (language delimited)
+      else ();
+  in gen_read SML pos text end;
 
 end;
 
--- a/src/Pure/PIDE/command.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/command.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -6,7 +6,7 @@
 
 signature COMMAND =
 sig
-  type blob = (string * string * (SHA1.digest * string list) option) Exn.result
+  type blob = (string * (SHA1.digest * string list) option) Exn.result
   val read_file: Path.T -> Position.T -> Path.T -> Token.file
   val read: (unit -> theory) -> Path.T -> blob list -> Token.T list -> Toplevel.transition
   type eval
@@ -87,7 +87,7 @@
 (* read *)
 
 type blob =
-  (string * string * (SHA1.digest * string list) option) Exn.result;  (*file, path, digest, lines*)
+  (string * (SHA1.digest * string list) option) Exn.result;  (*file node name, digest, lines*)
 
 fun read_file master_dir pos src_path =
   let
@@ -115,16 +115,16 @@
     [span] => span
       |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
         let
-          fun make_file src_path (Exn.Res (_, _, NONE)) =
+          fun make_file src_path (Exn.Res (_, NONE)) =
                 Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
-            | make_file src_path (Exn.Res (file_node, file_path, SOME (digest, lines))) =
-               (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_path)];
+            | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
+               (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
                 Exn.Res (blob_file src_path lines digest file_node))
             | make_file _ (Exn.Exn e) = Exn.Exn e;
           val src_paths = Keyword.command_files cmd path;
         in
           if null blobs then
-            map2 make_file src_paths (map (K (Exn.Res ("", "", NONE))) src_paths)
+            map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
           else if length src_paths = length blobs then
             map2 make_file src_paths blobs
           else error ("Misalignment of inlined files" ^ Position.here pos)
--- a/src/Pure/PIDE/command.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -15,7 +15,7 @@
 object Command
 {
   type Edit = (Option[Command], Option[Command])
-  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, File)])]
+  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, Text.Chunk)])]
 
 
 
@@ -60,10 +60,10 @@
 
   object Markup_Index
   {
-    val markup: Markup_Index = Markup_Index(false, "")
+    val markup: Markup_Index = Markup_Index(false, Text.Chunk.Default)
   }
 
-  sealed case class Markup_Index(status: Boolean, file_name: String)
+  sealed case class Markup_Index(status: Boolean, chunk_name: Text.Chunk.Name)
 
   object Markups
   {
@@ -81,6 +81,17 @@
     def add(index: Markup_Index, markup: Text.Markup): Markups =
       new Markups(rep + (index -> (this(index) + markup)))
 
+    def redirection_iterator: Iterator[Document_ID.Generic] =
+      for (Markup_Index(_, Text.Chunk.Id(id)) <- rep.keysIterator)
+        yield id
+
+    def redirect(other_id: Document_ID.Generic): Markups =
+      new Markups(
+        (for {
+          (Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator
+          if other_id == id
+        } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap)
+
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
       that match {
@@ -124,6 +135,9 @@
 
     def markup(index: Markup_Index): Markup_Tree = markups(index)
 
+    def redirect(other_command: Command): State =
+      new State(other_command, Nil, Results.empty, markups.redirect(other_command.id))
+
 
     def eq_content(other: State): Boolean =
       command.source == other.command.source &&
@@ -134,16 +148,19 @@
     private def add_status(st: Markup): State =
       copy(status = st :: status)
 
-    private def add_markup(status: Boolean, file_name: String, m: Text.Markup): State =
+    private def add_markup(status: Boolean, chunk_name: Text.Chunk.Name, m: Text.Markup): State =
     {
       val markups1 =
         if (status || Protocol.liberal_status_elements(m.info.name))
-          markups.add(Markup_Index(true, file_name), m)
+          markups.add(Markup_Index(true, chunk_name), m)
         else markups
-      copy(markups = markups1.add(Markup_Index(false, file_name), m))
+      copy(markups = markups1.add(Markup_Index(false, chunk_name), m))
     }
 
-    def + (valid_id: Document_ID.Generic => Boolean, message: XML.Elem): State =
+    def accumulate(
+        self_id: Document_ID.Generic => Boolean,
+        other_id: Document_ID.Generic => Option[(Text.Chunk.Id, Text.Chunk)],
+        message: XML.Elem): State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           (this /: msgs)((state, msg) =>
@@ -151,7 +168,7 @@
               case elem @ XML.Elem(markup, Nil) =>
                 state.
                   add_status(markup).
-                  add_markup(true, "", Text.Info(command.proper_range, elem))
+                  add_markup(true, Text.Chunk.Default, Text.Info(command.proper_range, elem))
               case _ =>
                 System.err.println("Ignored status message: " + msg)
                 state
@@ -163,19 +180,31 @@
               def bad(): Unit = System.err.println("Ignored report message: " + msg)
 
               msg match {
-                case XML.Elem(Markup(name,
-                  atts @ Position.Reported(id, file_name, symbol_range)), args)
-                if valid_id(id) =>
-                  command.chunks.get(file_name) match {
-                    case Some(chunk) =>
-                      chunk.incorporate(symbol_range) match {
+                case XML.Elem(
+                    Markup(name, atts @ Position.Reported(id, chunk_name, symbol_range)), args) =>
+
+                  val target =
+                    if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
+                      Some((chunk_name, command.chunks(chunk_name)))
+                    else if (chunk_name == Text.Chunk.Default) other_id(id)
+                    else None
+
+                  target match {
+                    case Some((target_name, target_chunk)) =>
+                      target_chunk.incorporate(symbol_range) match {
                         case Some(range) =>
                           val props = Position.purge(atts)
                           val info = Text.Info(range, XML.Elem(Markup(name, props), args))
-                          state.add_markup(false, file_name, info)
+                          state.add_markup(false, target_name, info)
                         case None => bad(); state
                       }
-                    case None => bad(); state
+                    case None =>
+                      chunk_name match {
+                        // FIXME workaround for static positions stemming from batch build
+                        case Text.Chunk.File(name) if name.endsWith(".thy") =>
+                        case _ => bad()
+                      }
+                      state
                   }
 
                 case XML.Elem(Markup(name, atts), args)
@@ -183,9 +212,9 @@
                   val range = command.proper_range
                   val props = Position.purge(atts)
                   val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
-                  state.add_markup(false, "", info)
+                  state.add_markup(false, Text.Chunk.Default, info)
 
-                case _ => /* FIXME bad(); */ state
+                case _ => bad(); state
               }
             })
         case XML.Elem(Markup(name, props), body) =>
@@ -197,9 +226,9 @@
               var st = copy(results = results + (i -> message1))
               if (Protocol.is_inlined(message)) {
                 for {
-                  (file_name, chunk) <- command.chunks
-                  range <- Protocol.message_positions(valid_id, chunk, message)
-                } st = st.add_markup(false, file_name, Text.Info(range, message2))
+                  (chunk_name, chunk) <- command.chunks.iterator
+                  range <- Protocol.message_positions(self_id, chunk_name, chunk, message)
+                } st = st.add_markup(false, chunk_name, Text.Info(range, message2))
               }
               st
 
@@ -214,49 +243,6 @@
 
   /** static content **/
 
-  /* text chunks */
-
-  abstract class Chunk
-  {
-    def file_name: String
-    def length: Int
-    def range: Text.Range
-    def decode(symbol_range: Symbol.Range): Text.Range
-
-    def incorporate(symbol_range: Symbol.Range): Option[Text.Range] =
-    {
-      def inc(r: Symbol.Range): Option[Text.Range] =
-        range.try_restrict(decode(r)) match {
-          case Some(r1) if !r1.is_singularity => Some(r1)
-          case _ => None
-        }
-     inc(symbol_range) orElse inc(symbol_range - 1)
-    }
-  }
-
-  // file name and position information, *without* persistent text
-  class File(val file_name: String, text: CharSequence) extends Chunk
-  {
-    val length = text.length
-    val range = Text.Range(0, length)
-    private val symbol_index = Symbol.Index(text)
-    def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range)
-
-    private val hash: Int = (file_name, length, symbol_index).hashCode
-    override def hashCode: Int = hash
-    override def equals(that: Any): Boolean =
-      that match {
-        case other: File =>
-          hash == other.hash &&
-          file_name == other.file_name &&
-          length == other.length &&
-          symbol_index == other.symbol_index
-        case _ => false
-      }
-    override def toString: String = "Command.File(" + file_name + ")"
-  }
-
-
   /* make commands */
 
   def name(span: List[Token]): String =
@@ -344,7 +330,6 @@
     val source: String,
     val init_results: Command.Results,
     val init_markup: Markup_Tree)
-  extends Command.Chunk
 {
   /* classification */
 
@@ -373,27 +358,24 @@
   def blobs_digests: List[SHA1.Digest] =
     for (Exn.Res((_, Some((digest, _)))) <- blobs) yield digest
 
-  val chunks: Map[String, Command.Chunk] =
-    (("" -> this) ::
-      (for (Exn.Res((name, Some((_, file)))) <- blobs) yield (name.node -> file))).toMap
+
+  /* source chunks */
+
+  val chunk: Text.Chunk = Text.Chunk(source)
 
-
-  /* source */
-
-  def file_name: String = ""
+  val chunks: Map[Text.Chunk.Name, Text.Chunk] =
+    ((Text.Chunk.Default -> chunk) ::
+      (for (Exn.Res((name, Some((_, file)))) <- blobs)
+        yield (Text.Chunk.File(name.node) -> file))).toMap
 
   def length: Int = source.length
-  val range: Text.Range = Text.Range(0, length)
+  def range: Text.Range = chunk.range
 
   val proper_range: Text.Range =
     Text.Range(0, (length /: span.reverse.iterator.takeWhile(_.is_improper))(_ - _.source.length))
 
   def source(range: Text.Range): String = source.substring(range.start, range.stop)
 
-  private lazy val symbol_index = Symbol.Index(source)
-  def decode(symbol_offset: Symbol.Offset): Text.Offset = symbol_index.decode(symbol_offset)
-  def decode(symbol_range: Symbol.Range): Text.Range = symbol_index.decode(symbol_range)
-
 
   /* accumulated results */
 
--- a/src/Pure/PIDE/document.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -18,7 +18,7 @@
   type state
   val init_state: state
   val define_blob: string -> string -> state -> state
-  type blob_digest = (string * string * string option) Exn.result
+  type blob_digest = (string * string option) Exn.result
   val define_command: Document_ID.command -> string -> blob_digest list -> string ->
     state -> state
   val remove_versions: Document_ID.version list -> state -> state
@@ -219,8 +219,7 @@
 
 (** main state -- document structure and execution process **)
 
-type blob_digest =
-  (string * string * string option) Exn.result;  (* file node name, path, raw digest*)
+type blob_digest = (string * string option) Exn.result;  (*file node name, raw digest*)
 
 type execution =
  {version_id: Document_ID.version,  (*static version id*)
@@ -293,8 +292,8 @@
   | SOME content => content);
 
 fun resolve_blob state (blob_digest: blob_digest) =
-  blob_digest |> Exn.map_result (fn (file, path, raw_digest) =>
-    (file, path, Option.map (the_blob state) raw_digest));
+  blob_digest |> Exn.map_result (fn (file_node, raw_digest) =>
+    (file_node, Option.map (the_blob state) raw_digest));
 
 
 (* commands *)
@@ -343,7 +342,7 @@
     val blobs' =
       (commands', Symtab.empty) |->
         Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
-          fold (fn Exn.Res (_, _, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
+          fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
 
   in (versions', blobs', commands', execution) end);
 
--- a/src/Pure/PIDE/document.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -45,7 +45,7 @@
 
   /* document blobs: auxiliary files */
 
-  sealed case class Blob(bytes: Bytes, file: Command.File, changed: Boolean)
+  sealed case class Blob(bytes: Bytes, chunk: Text.Chunk, changed: Boolean)
   {
     def unchanged: Blob = copy(changed = false)
   }
@@ -483,11 +483,19 @@
   }
 
   final case class State private(
+    /*reachable versions*/
     val versions: Map[Document_ID.Version, Version] = Map.empty,
-    val blobs: Set[SHA1.Digest] = Set.empty,   // inlined files
-    val commands: Map[Document_ID.Command, Command.State] = Map.empty,  // static markup from define_command
-    val execs: Map[Document_ID.Exec, Command.State] = Map.empty,  // dynamic markup from execution
+    /*inlined auxiliary files*/
+    val blobs: Set[SHA1.Digest] = Set.empty,
+    /*static markup from define_command*/
+    val commands: Map[Document_ID.Command, Command.State] = Map.empty,
+    /*dynamic markup from execution*/
+    val execs: Map[Document_ID.Exec, Command.State] = Map.empty,
+    /*command-exec assignment for each version*/
     val assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
+    /*commands with markup produced by other commands (imm_succs)*/
+    val commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long,
+    /*explicit (linear) history*/
     val history: History = History.init)
   {
     private def fail[A]: A = throw new State.Fail(this)
@@ -524,23 +532,35 @@
     def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
     def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
 
-    def valid_id(st: Command.State)(id: Document_ID.Generic): Boolean =
+    private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean =
       id == st.command.id ||
       (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false })
 
+    private def other_id(id: Document_ID.Generic): Option[(Text.Chunk.Id, Text.Chunk)] =
+      (execs.get(id) orElse commands.get(id)).map(st =>
+        ((Text.Chunk.Id(st.command.id), st.command.chunk)))
+
+    private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] =
+      (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) =>
+        graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) })
+
     def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
+    {
       execs.get(id) match {
         case Some(st) =>
-          val new_st = st + (valid_id(st), message)
-          (new_st, copy(execs = execs + (id -> new_st)))
+          val new_st = st.accumulate(self_id(st), other_id _, message)
+          val execs1 = execs + (id -> new_st)
+          (new_st, copy(execs = execs1, commands_redirection = redirection(new_st)))
         case None =>
           commands.get(id) match {
             case Some(st) =>
-              val new_st = st + (valid_id(st), message)
-              (new_st, copy(commands = commands + (id -> new_st)))
+              val new_st = st.accumulate(self_id(st), other_id _, message)
+              val commands1 = commands + (id -> new_st)
+              (new_st, copy(commands = commands1, commands_redirection = redirection(new_st)))
             case None => fail
           }
       }
+    }
 
     def assign(id: Document_ID.Version, update: Assign_Update): (List[Command], State) =
     {
@@ -629,27 +649,48 @@
             execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
         }
       }
-      copy(versions = versions1, blobs = blobs1, commands = commands1, execs = execs1,
+      copy(
+        versions = versions1,
+        blobs = blobs1,
+        commands = commands1,
+        execs = execs1,
+        commands_redirection = commands_redirection.restrict(commands1.isDefinedAt(_)),
         assignments = assignments1)
     }
 
-    def command_states(version: Version, command: Command): List[Command.State] =
+    private def command_states_self(version: Version, command: Command)
+      : List[(Document_ID.Generic, Command.State)] =
     {
       require(is_assigned(version))
       try {
         the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil)
-          .map(the_dynamic_state(_)) match {
+          .map(id => id -> the_dynamic_state(id)) match {
             case Nil => fail
-            case states => states
+            case res => res
           }
       }
       catch {
         case _: State.Fail =>
-          try { List(the_static_state(command.id)) }
-          catch { case _: State.Fail => List(command.init_state) }
+          try { List(command.id -> the_static_state(command.id)) }
+          catch { case _: State.Fail => List(command.id -> command.init_state) }
       }
     }
 
+    def command_states(version: Version, command: Command): List[Command.State] =
+    {
+      val self = command_states_self(version, command)
+      val others =
+        if (commands_redirection.defined(command.id)) {
+          (for {
+            command_id <- commands_redirection.imm_succs(command.id).iterator
+            (id, st) <- command_states_self(version, the_static_state(command_id).command)
+            if !self.exists(_._1 == id)
+          } yield (id, st)).toMap.valuesIterator.toList
+        }
+        else Nil
+      self.map(_._2) ::: others.map(_.redirect(command))
+    }
+
     def command_results(version: Version, command: Command): Command.Results =
       Command.State.merge_results(command_states(version, command))
 
@@ -731,15 +772,15 @@
           status: Boolean = false): List[Text.Info[A]] =
         {
           val former_range = revert(range)
-          val (file_name, command_iterator) =
+          val (chunk_name, command_iterator) =
             load_commands match {
-              case command :: _ => (node_name.node, Iterator((command, 0)))
-              case _ => ("", node.command_iterator(former_range))
+              case command :: _ => (Text.Chunk.File(node_name.node), Iterator((command, 0)))
+              case _ => (Text.Chunk.Default, node.command_iterator(former_range))
             }
-          val markup_index = Command.Markup_Index(status, file_name)
+          val markup_index = Command.Markup_Index(status, chunk_name)
           (for {
             (command, command_start) <- command_iterator
-            chunk <- command.chunks.get(file_name).iterator
+            chunk <- command.chunks.get(chunk_name).iterator
             states = state.command_states(version, command)
             res = result(states)
             range = (former_range - command_start).restrict(chunk.range)
--- a/src/Pure/PIDE/markup.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -63,6 +63,7 @@
   val fbreakN: string val fbreak: T
   val itemN: string val item: T
   val hiddenN: string val hidden: T
+  val system_optionN: string
   val theoryN: string
   val classN: string
   val type_nameN: string
@@ -358,7 +359,9 @@
 val (hiddenN, hidden) = markup_elem "hidden";
 
 
-(* logical entities *)
+(* formal entities *)
+
+val system_optionN = "system_option";
 
 val theoryN = "theory";
 val classN = "class";
--- a/src/Pure/PIDE/protocol.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/protocol.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -34,7 +34,7 @@
           YXML.parse_body blobs_yxml |>
             let open XML.Decode in
               list (variant
-               [fn ([], a) => Exn.Res (triple string string (option string) a),
+               [fn ([], a) => Exn.Res (pair string (option string) a),
                 fn ([], a) => Exn.Exn (ERROR (string a))])
             end;
       in
--- a/src/Pure/PIDE/protocol.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -95,9 +95,9 @@
 
     def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
     def is_running: Boolean = runs != 0
+    def is_warned: Boolean = warned
+    def is_failed: Boolean = failed
     def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
-    def is_warned: Boolean = is_finished && warned
-    def is_failed: Boolean = failed
   }
 
   val proper_status_elements =
@@ -127,9 +127,9 @@
   /* node status */
 
   sealed case class Node_Status(
-    unprocessed: Int, running: Int, finished: Int, warned: Int, failed: Int)
+    unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int)
   {
-    def total: Int = unprocessed + running + finished + warned + failed
+    def total: Int = unprocessed + running + warned + failed + finished
   }
 
   def node_status(
@@ -137,20 +137,20 @@
   {
     var unprocessed = 0
     var running = 0
-    var finished = 0
     var warned = 0
     var failed = 0
+    var finished = 0
     for (command <- node.commands.iterator) {
       val states = state.command_states(version, command)
       val status = Status.merge(states.iterator.map(_.protocol_status))
 
       if (status.is_running) running += 1
       else if (status.is_warned) warned += 1
+      else if (status.is_failed) failed += 1
       else if (status.is_finished) finished += 1
-      else if (status.is_failed) failed += 1
       else unprocessed += 1
     }
-    Node_Status(unprocessed, running, finished, warned, failed)
+    Node_Status(unprocessed, running, warned, failed, finished)
   }
 
 
@@ -301,14 +301,15 @@
     Document.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
 
   def message_positions(
-    valid_id: Document_ID.Generic => Boolean,
-    chunk: Command.Chunk,
+    self_id: Document_ID.Generic => Boolean,
+    chunk_name: Text.Chunk.Name,
+    chunk: Text.Chunk,
     message: XML.Elem): Set[Text.Range] =
   {
     def elem_positions(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
       props match {
-        case Position.Reported(id, file_name, symbol_range)
-        if valid_id(id) && file_name == chunk.file_name =>
+        case Position.Reported(id, name, symbol_range)
+        if self_id(id) && name == chunk_name =>
           chunk.incorporate(symbol_range) match {
             case Some(range) => set + range
             case _ => set
@@ -352,8 +353,7 @@
       val encode_blob: T[Command.Blob] =
         variant(List(
           { case Exn.Res((a, b)) =>
-              (Nil, triple(string, string, option(string))(
-                (a.node, Isabelle_System.posix_path_url(a.node), b.map(p => p._1.toString)))) },
+              (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
       YXML.string_of_body(list(encode_blob)(command.blobs))
     }
--- a/src/Pure/PIDE/text.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/PIDE/text.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -71,6 +71,44 @@
   }
 
 
+  /* named chunks with sparse symbol index */
+
+  object Chunk
+  {
+    sealed abstract class Name
+    case object Default extends Name
+    case class Id(id: Document_ID.Generic) extends Name
+    case class File(name: String) extends Name
+
+    def apply(text: CharSequence): Chunk =
+      new Chunk(Range(0, text.length), Symbol.Index(text))
+  }
+
+  final class Chunk private(val range: Range, private val symbol_index: Symbol.Index)
+  {
+    override def hashCode: Int = (range, symbol_index).hashCode
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Chunk =>
+          range == other.range &&
+          symbol_index == other.symbol_index
+        case _ => false
+      }
+
+    def decode(symbol_offset: Symbol.Offset): Offset = symbol_index.decode(symbol_offset)
+    def decode(symbol_range: Symbol.Range): Range = symbol_index.decode(symbol_range)
+    def incorporate(symbol_range: Symbol.Range): Option[Range] =
+    {
+      def in(r: Symbol.Range): Option[Range] =
+        range.try_restrict(decode(r)) match {
+          case Some(r1) if !r1.is_singularity => Some(r1)
+          case _ => None
+        }
+     in(symbol_range) orElse in(symbol_range - 1)
+    }
+  }
+
+
   /* perspective */
 
   object Perspective
--- a/src/Pure/System/isabelle_system.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -10,8 +10,9 @@
 
 import java.util.regex.Pattern
 import java.io.{File => JFile, BufferedReader, InputStreamReader,
-  BufferedWriter, OutputStreamWriter}
-import java.nio.file.Files
+  BufferedWriter, OutputStreamWriter, IOException}
+import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
+import java.nio.file.attribute.BasicFileAttributes
 import java.net.{URL, URLDecoder, MalformedURLException}
 
 import scala.util.matching.Regex
@@ -104,7 +105,7 @@
             shell_prefix ::: List(system_home + "/bin/isabelle", "getenv", "-d", dump.toString)
           val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*))
           if (rc != 0) error(output)
-  
+
           val entries =
             (for (entry <- File.read(dump) split "\0" if entry != "") yield {
               val i = entry.indexOf('=')
@@ -394,6 +395,47 @@
   }
 
 
+  /* tmp dirs */
+
+  def rm_tree(root: JFile)
+  {
+    root.delete
+    if (root.isDirectory) {
+      Files.walkFileTree(root.toPath,
+        new SimpleFileVisitor[JPath] {
+          override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult =
+          {
+            Files.delete(file)
+            FileVisitResult.CONTINUE
+          }
+
+          override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult =
+          {
+            if (e == null) {
+              Files.delete(dir)
+              FileVisitResult.CONTINUE
+            }
+            else throw e
+          }
+        }
+      )
+    }
+  }
+
+  def tmp_dir(name: String): JFile =
+  {
+    val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile
+    dir.deleteOnExit
+    dir
+  }
+
+  def with_tmp_dir[A](name: String)(body: JFile => A): A =
+  {
+    val dir = tmp_dir(name)
+    try { body(dir) } finally { rm_tree(dir) }
+  }
+
+
   /* bash */
 
   final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int)
@@ -444,35 +486,6 @@
   def bash(script: String): Bash_Result = bash_env(null, null, script)
 
 
-  /* tmp dirs */
-
-  private def system_command(cmd: String)
-  {
-    val res = bash(cmd)
-    if (res.rc != 0)
-      error(cat_lines(("System command failed: " + cmd) :: res.out_lines ::: res.err_lines))
-  }
-
-  def rm_tree(dir: JFile)
-  {
-    dir.delete
-    if (dir.isDirectory) system_command("rm -r -f " + shell_path(dir))
-  }
-
-  def tmp_dir(name: String): JFile =
-  {
-    val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile
-    dir.deleteOnExit
-    dir
-  }
-
-  def with_tmp_dir[A](name: String)(body: JFile => A): A =
-  {
-    val dir = tmp_dir(name)
-    try { body(dir) } finally { rm_tree(dir) }
-  }
-
-
   /* system tools */
 
   def isabelle_tool(name: String, args: String*): (String, Int) =
--- a/src/Pure/System/options.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/System/options.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -13,6 +13,7 @@
   val unknownT: string
   type T
   val empty: T
+  val markup: T -> string * Position.T -> Markup.T
   val typ: T -> string -> string
   val bool: T -> string -> bool
   val int: T -> string -> int
@@ -22,10 +23,11 @@
   val put_int: string -> int -> T -> T
   val put_real: string -> real -> T -> T
   val put_string: string -> string -> T -> T
-  val declare: {name: string, typ: string, value: string} -> T -> T
+  val declare: {pos: Position.T, name: string, typ: string, value: string} -> T -> T
   val update: string -> string -> T -> T
   val decode: XML.body -> T
   val default: unit -> T
+  val default_markup: string * Position.T -> Markup.T
   val default_typ: string -> string
   val default_bool: string -> bool
   val default_int: string -> int
@@ -53,7 +55,7 @@
 val stringT = "string";
 val unknownT = "unknown";
 
-datatype T = Options of {typ: string, value: string} Symtab.table;
+datatype T = Options of {pos: Position.T, typ: string, value: string} Symtab.table;
 
 val empty = Options Symtab.empty;
 
@@ -73,6 +75,17 @@
   end;
 
 
+(* markup *)
+
+fun markup options (name, pos) =
+  let
+    val opt =
+      check_name options name
+        handle ERROR msg => error (msg ^ Position.here pos);
+    val props = Position.def_properties_of (#pos opt);
+  in Markup.properties props (Markup.entity Markup.system_optionN name) end;
+
+
 (* typ *)
 
 fun typ options name = #typ (check_name options name);
@@ -82,7 +95,7 @@
 
 fun put T print name x (options as Options tab) =
   let val opt = check_type options name T
-  in Options (Symtab.update (name, {typ = #typ opt, value = print x}) tab) end;
+  in Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = print x}) tab) end;
 
 fun get T parse options name =
   let val opt = check_type options name T in
@@ -118,29 +131,39 @@
     else ()
   end;
 
-fun declare {name, typ, value} (Options tab) =
+fun declare {pos, name, typ, value} (Options tab) =
   let
-    val options' = Options (Symtab.update_new (name, {typ = typ, value = value}) tab)
-      handle Symtab.DUP _ => error ("Duplicate declaration of system option " ^ quote name);
+    val options' =
+      (case Symtab.lookup tab name of
+        SOME other =>
+          error ("Duplicate declaration of system option " ^ quote name ^ Position.here pos ^
+            Position.here (#pos other))
+      | NONE => Options (Symtab.update (name, {pos = pos, typ = typ, value = value}) tab));
     val _ =
       typ = boolT orelse typ = intT orelse typ = realT orelse typ = stringT orelse
-        error ("Unknown type for system option " ^ quote name ^ " : " ^ quote typ);
+        error ("Unknown type for system option " ^ quote name ^ " : " ^ quote typ ^
+          Position.here pos);
     val _ = check_value options' name;
   in options' end;
 
 fun update name value (options as Options tab) =
   let
     val opt = check_name options name;
-    val options' = Options (Symtab.update (name, {typ = #typ opt, value = value}) tab);
+    val options' =
+      Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = value}) tab);
     val _ = check_value options' name;
   in options' end;
 
 
 (* decode *)
 
-fun decode body =
-  fold (declare o (fn (name, typ, value) => {name = name, typ = typ, value = value}))
-    (let open XML.Decode in list (triple string string string) end body) empty;
+fun decode_opt body =
+  let open XML.Decode
+  in list (pair properties (pair string (pair string string))) end body
+  |> map (fn (props, (name, (typ, value))) =>
+      {pos = Position.of_properties props, name = name, typ = typ, value = value});
+
+fun decode body = fold declare (decode_opt body) empty;
 
 
 
@@ -160,6 +183,7 @@
     SOME options => options
   | NONE => err_no_default ());
 
+fun default_markup arg = markup (default ()) arg;
 fun default_typ name = typ (default ()) name;
 fun default_bool name = bool (default ()) name;
 fun default_int name = int (default ()) name;
--- a/src/Pure/System/options.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/System/options.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -29,8 +29,15 @@
   case object String extends Type
   case object Unknown extends Type
 
-  case class Opt(public: Boolean, name: String, typ: Type, value: String, default_value: String,
-    description: String, section: String)
+  case class Opt(
+    public: Boolean,
+    pos: Position.T,
+    name: String,
+    typ: Type,
+    value: String,
+    default_value: String,
+    description: String,
+    section: String)
   {
     private def print(default: Boolean): String =
     {
@@ -88,8 +95,8 @@
         { case _ ~ a => (options: Options) => options.set_section(a) } |
       opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ keyword(":") ~ option_type ~
       keyword("=") ~ option_value ~ (keyword("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
-        { case a ~ _ ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
-            (options: Options) => options.declare(a.isDefined, b, c, d, e) }
+        { case a ~ pos ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
+            (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
     }
 
     val prefs_entry: Parser[Options => Options] =
@@ -260,11 +267,18 @@
     }
   }
 
-  def declare(public: Boolean, name: String, typ_name: String, value: String, description: String)
-    : Options =
+  def declare(
+    public: Boolean,
+    pos: Position.T,
+    name: String,
+    typ_name: String,
+    value: String,
+    description: String): Options =
   {
     options.get(name) match {
-      case Some(_) => error("Duplicate declaration of option " + quote(name))
+      case Some(other) =>
+        error("Duplicate declaration of option " + quote(name) + Position.here(pos) +
+          Position.here(other.pos))
       case None =>
         val typ =
           typ_name match {
@@ -272,9 +286,11 @@
             case "int" => Options.Int
             case "real" => Options.Real
             case "string" => Options.String
-            case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
+            case _ =>
+              error("Unknown type for option " + quote(name) + " : " + quote(typ_name) +
+                Position.here(pos))
           }
-        val opt = Options.Opt(public, name, typ, value, value, description, section)
+        val opt = Options.Opt(public, pos, name, typ, value, value, description, section)
         (new Options(options + (name -> opt), section)).check_value(name)
     }
   }
@@ -282,10 +298,10 @@
   def add_permissive(name: String, value: String): Options =
   {
     if (options.isDefinedAt(name)) this + (name, value)
-    else
-      new Options(
-        options +
-          (name -> Options.Opt(false, name, Options.Unknown, value, value, "", "")), section)
+    else {
+      val opt = Options.Opt(false, Position.none, name, Options.Unknown, value, value, "", "")
+      new Options(options + (name -> opt), section)
+    }
   }
 
   def + (name: String, value: String): Options =
@@ -330,11 +346,11 @@
   def encode: XML.Body =
   {
     val opts =
-      for ((name, opt) <- options.toList; if !opt.unknown)
-        yield (name, opt.typ.print, opt.value)
+      for ((_, opt) <- options.toList; if !opt.unknown)
+        yield (opt.pos, (opt.name, (opt.typ.print, opt.value)))
 
-    import XML.Encode.{string => str, _}
-    list(triple(str, str, str))(opts)
+    import XML.Encode.{string => string_, _}
+    list(pair(properties, pair(string_, pair(string_, string_))))(opts)
   }
 
 
--- a/src/Pure/Thy/thy_syntax.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -271,7 +271,7 @@
       Exn.capture {
         val name =
           Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file_name)))
-        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.file)))
+        val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
         (name, blob)
       })
   }
--- a/src/Pure/Tools/build.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/Tools/build.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -203,16 +203,14 @@
 
   private object Parser extends Parse.Parser
   {
-    def entry(pos: Position.T): Parser[Entry] = chapter(pos) | session_entry(pos)
-
-    def chapter(pos: Position.T): Parser[Chapter] =
+    val chapter: Parser[Chapter] =
     {
       val chapter_name = atom("chapter name", _.is_name)
 
       command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
     }
 
-    def session_entry(pos: Position.T): Parser[Session_Entry] =
+    val session_entry: Parser[Session_Entry] =
     {
       val session_name = atom("session name", _.is_name)
 
@@ -234,7 +232,7 @@
               ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
               rep1(theories) ~
               ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^
-        { case _ ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
+        { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
             Session_Entry(pos, a, b, c, d, e, f, g, h) }
     }
 
@@ -242,7 +240,7 @@
     {
       val toks = root_syntax.scan(File.read(root))
 
-      parse_all(rep(entry(root.position)), Token.reader(toks, root.implode)) match {
+      parse_all(rep(chapter | session_entry), Token.reader(toks, root.implode)) match {
         case Success(result, _) =>
           var chapter = chapter_default
           val entries = new mutable.ListBuffer[(String, Session_Entry)]
--- a/src/Pure/Tools/find_theorems.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -206,7 +206,7 @@
     val goal' = Thm.transfer thy' goal;
 
     fun limited_etac thm i =
-      Seq.take (Options.default_int @{option find_theorems_tac_limit}) o etac thm i;
+      Seq.take (Options.default_int @{system_option find_theorems_tac_limit}) o etac thm i;
     fun try_thm thm =
       if Thm.no_prems thm then rtac thm 1 goal'
       else
@@ -405,7 +405,7 @@
           else raw_matches;
 
         val len = length matches;
-        val lim = the_default (Options.default_int @{option find_theorems_limit}) opt_limit;
+        val lim = the_default (Options.default_int @{system_option find_theorems_limit}) opt_limit;
       in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
 
     val find =
--- a/src/Pure/Tools/proof_general_pure.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -17,49 +17,49 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    @{option show_types}
+    @{system_option show_types}
     "show-types"
     "Include types in display of Isabelle terms";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    @{option show_sorts}
+    @{system_option show_sorts}
     "show-sorts"
     "Include sorts in display of Isabelle types";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    @{option show_consts}
+    @{system_option show_consts}
     "show-consts"
     "Show types of consts in Isabelle goal display";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    @{option names_long}
+    @{system_option names_long}
     "long-names"
     "Show fully qualified names in Isabelle terms";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    @{option show_brackets}
+    @{system_option show_brackets}
     "show-brackets"
     "Show full bracketing in Isabelle terms";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    @{option show_main_goal}
+    @{system_option show_main_goal}
     "show-main-goal"
     "Show main goal in proof state display";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_display
     NONE
-    @{option eta_contract}
+    @{system_option eta_contract}
     "eta-contract"
     "Print terms eta-contracted";
 
@@ -69,7 +69,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_advanced_display
     NONE
-    @{option goals_limit}
+    @{system_option goals_limit}
     "goals-limit"
     "Setting for maximum number of subgoals to be printed";
 
@@ -85,7 +85,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_advanced_display
     NONE
-    @{option show_question_marks}
+    @{system_option show_question_marks}
     "show-question-marks"
     "Show leading question mark of variable name";
 
@@ -123,7 +123,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    @{option ML_exception_trace}
+    @{system_option ML_exception_trace}
     "debugging"
     "Whether to enable exception trace for toplevel command execution";
 
@@ -140,14 +140,14 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_proof
     (SOME "true")
-    @{option quick_and_dirty}
+    @{system_option quick_and_dirty}
     "quick-and-dirty"
     "Take a few short cuts";
 
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_proof
     NONE
-    @{option skip_proofs}
+    @{system_option skip_proofs}
     "skip-proofs"
     "Skip over proofs";
 
--- a/src/Tools/jEdit/src/document_model.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -119,7 +119,7 @@
         for {
           cmd <- snapshot.node.load_commands
           blob_name <- cmd.blobs_names
-          blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node)
+          blob_buffer <- JEdit_Lib.jedit_buffer(blob_name)
           if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
           start <- snapshot.node.command_start(cmd)
           range = snapshot.convert(cmd.proper_range + start)
@@ -138,7 +138,7 @@
 
   /* blob */
 
-  private var _blob: Option[(Bytes, Command.File)] = None  // owned by Swing thread
+  private var _blob: Option[(Bytes, Text.Chunk)] = None  // owned by Swing thread
 
   private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
 
@@ -146,17 +146,17 @@
     Swing_Thread.require {
       if (is_theory) None
       else {
-        val (bytes, file) =
+        val (bytes, chunk) =
           _blob match {
             case Some(x) => x
             case None =>
               val bytes = PIDE.resources.file_content(buffer)
-              val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength))
-              _blob = Some((bytes, file))
-              (bytes, file)
+              val chunk = Text.Chunk(buffer.getSegment(0, buffer.getLength))
+              _blob = Some((bytes, chunk))
+              (bytes, chunk)
           }
         val changed = pending_edits.is_pending()
-        Some(Document.Blob(bytes, file, changed))
+        Some(Document.Blob(bytes, chunk, changed))
       }
     }
 
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -52,7 +52,7 @@
   {
     Swing_Thread.require()
 
-    JEdit_Lib.jedit_buffer(name.node) match {
+    JEdit_Lib.jedit_buffer(name) match {
       case Some(buffer) =>
         PIDE.document_model(buffer) match {
           case Some(model) => model.snapshot
@@ -159,6 +159,55 @@
 
   /* hyperlinks */
 
+  def hyperlink_url(name: String): Hyperlink =
+    new Hyperlink {
+      def follow(view: View) =
+        default_thread_pool.submit(() =>
+          try { Isabelle_System.open(name) }
+          catch {
+            case exn: Throwable =>
+              GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
+          })
+      override def toString: String = "URL " + quote(name)
+    }
+
+  def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
+    new Hyperlink {
+      def follow(view: View) = goto_file(view, name, line, column)
+      override def toString: String = "file " + quote(name)
+    }
+
+  def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
+    : Option[Hyperlink] =
+  {
+    val opt_name =
+      if (Path.is_wellformed(source_name)) {
+        if (Path.is_valid(source_name)) {
+          val path = Path.explode(source_name)
+          Some(Isabelle_System.platform_path(Isabelle_System.source_file(path) getOrElse path))
+        }
+        else None
+      }
+      else Some(source_name)
+
+    opt_name match {
+      case Some(name) =>
+        JEdit_Lib.jedit_buffer(name) match {
+          case Some(buffer) if offset > 0 =>
+            val (line, column) =
+              JEdit_Lib.buffer_lock(buffer) {
+                ((1, 1) /:
+                  (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
+                    zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
+                      Symbol.advance_line_column)
+              }
+            Some(hyperlink_file(name, line, column))
+          case _ => Some(hyperlink_file(name, line))
+        }
+      case None => None
+    }
+  }
+
   override def hyperlink_command(
     snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0): Option[Hyperlink] =
   {
@@ -171,9 +220,9 @@
           val sources_iterator =
             node.commands.iterator.takeWhile(_ != command).map(_.source) ++
               (if (offset == 0) Iterator.empty
-               else Iterator.single(command.source(Text.Range(0, command.decode(offset)))))
+               else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
           val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column)
-          Some(new Hyperlink { def follow(view: View) { goto_file(view, file_name, line, column) } })
+          Some(hyperlink_file(file_name, line, column))
       }
     }
   }
@@ -188,43 +237,4 @@
       case None => None
     }
   }
-
-  def hyperlink_file(name: String, line: Int = 0, column: Int = 0): Hyperlink =
-    new Hyperlink { def follow(view: View) = goto_file(view, name, line, column) }
-
-  def hyperlink_source_file(source_name: String, line: Int, offset: Symbol.Offset)
-    : Option[Hyperlink] =
-  {
-    if (Path.is_valid(source_name)) {
-      Isabelle_System.source_file(Path.explode(source_name)) match {
-        case Some(path) =>
-          val name = Isabelle_System.platform_path(path)
-          JEdit_Lib.jedit_buffer(name) match {
-            case Some(buffer) if offset > 0 =>
-              val (line, column) =
-                JEdit_Lib.buffer_lock(buffer) {
-                  ((1, 1) /:
-                    (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
-                      zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(
-                        Symbol.advance_line_column)
-                }
-              Some(hyperlink_file(name, line, column))
-            case _ => Some(hyperlink_file(name, line))
-          }
-        case None => None
-      }
-    }
-    else None
-  }
-
-  def hyperlink_url(name: String): Hyperlink =
-    new Hyperlink {
-      def follow(view: View) =
-        default_thread_pool.submit(() =>
-          try { Isabelle_System.open(name) }
-          catch {
-            case exn: Throwable =>
-              GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
-          })
-    }
 }
--- a/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -120,6 +120,9 @@
   def jedit_buffer(name: String): Option[Buffer] =
     jedit_buffers().find(buffer => buffer_name(buffer) == name)
 
+  def jedit_buffer(name: Document.Node.Name): Option[Buffer] =
+    jedit_buffer(name.node)
+
   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
 
   def jedit_text_areas(view: View): Iterator[JEditTextArea] =
--- a/src/Tools/jEdit/src/jedit_resources.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -57,7 +57,7 @@
   override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
   {
     Swing_Thread.now {
-      JEdit_Lib.jedit_buffer(name.node) match {
+      JEdit_Lib.jedit_buffer(name) match {
         case Some(buffer) =>
           JEdit_Lib.buffer_lock(buffer) {
             Some(f(buffer.getSegment(0, buffer.getLength)))
@@ -120,7 +120,6 @@
   override def commit(change: Session.Change)
   {
     if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() }
-    if (change.deps_changed) PIDE.deps_changed()
   }
 }
 
--- a/src/Tools/jEdit/src/rendering.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -321,15 +321,18 @@
 
   /* hyperlinks */
 
+  private def jedit_file(name: String): String =
+    if (Path.is_valid(name))
+      PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
+    else name
+
   def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   {
     snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
       range, Vector.empty, Rendering.hyperlink_elements, _ =>
         {
-          case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
-          if Path.is_valid(name) =>
-            val jedit_file = PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
-            val link = PIDE.editor.hyperlink_file(jedit_file)
+          case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
+            val link = PIDE.editor.hyperlink_file(jedit_file(name))
             Some(links :+ Text.Info(snapshot.convert(info_range), link))
 
           case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
@@ -457,10 +460,11 @@
                 "\n" + t.message
               else ""
             Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
-          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
-          if Path.is_valid(name) =>
-            val jedit_file = PIDE.resources.append(snapshot.node_name.master_dir, Path.explode(name))
-            val text = "path " + quote(name) + "\nfile " + quote(jedit_file)
+          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
+            val file = jedit_file(name)
+            val text =
+              if (name == file) "file " + quote(file)
+              else "path " + quote(name) + "\nfile " + quote(file)
             Some(add(prev, r, (true, XML.Text(text))))
           case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
             Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
--- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Apr 08 23:16:00 2014 +0200
@@ -41,7 +41,7 @@
           if (in_checkbox(peer.indexToLocation(index), point)) {
             if (clicks == 1) {
               for {
-                buffer <- JEdit_Lib.jedit_buffer(listData(index).node)
+                buffer <- JEdit_Lib.jedit_buffer(listData(index))
                 model <- PIDE.document_model(buffer)
               } model.node_required = !model.node_required
             }
--- a/src/Tools/quickcheck.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/quickcheck.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -95,7 +95,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    @{option auto_quickcheck}
+    @{system_option auto_quickcheck}
     "auto-quickcheck"
     "Run Quickcheck automatically";
 
@@ -584,7 +584,7 @@
   end
   |> `(fn (outcome_code, _) => outcome_code = genuineN);
 
-val _ = Try.tool_setup (quickcheckN, (20, @{option auto_quickcheck}, try_quickcheck));
+val _ = Try.tool_setup (quickcheckN, (20, @{system_option auto_quickcheck}, try_quickcheck));
 
 end;
 
--- a/src/Tools/solve_direct.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/solve_direct.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -37,7 +37,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    @{option auto_solve_direct}
+    @{system_option auto_solve_direct}
     "auto-solve-direct"
     ("Run " ^ quote solve_directN ^ " automatically");
 
@@ -115,6 +115,6 @@
 
 fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
 
-val _ = Try.tool_setup (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct));
+val _ = Try.tool_setup (solve_directN, (10, @{system_option auto_solve_direct}, try_solve_direct));
 
 end;
--- a/src/Tools/try.ML	Tue Apr 08 18:48:10 2014 +0200
+++ b/src/Tools/try.ML	Tue Apr 08 23:16:00 2014 +0200
@@ -32,7 +32,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     (SOME "4.0")
-    @{option auto_time_limit}
+    @{system_option auto_time_limit}
     "auto-try-time-limit"
     "Time limit for automatically tried tools (in seconds)"
 
@@ -103,7 +103,7 @@
 
 val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
   let
-    val auto_time_limit = Options.default_real @{option auto_time_limit}
+    val auto_time_limit = Options.default_real @{system_option auto_time_limit}
   in
     if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then
       TimeLimit.timeLimit (seconds auto_time_limit) auto_try state
@@ -120,7 +120,7 @@
     (fn {command_name, ...} =>
       if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
         SOME
-         {delay = SOME (seconds (Options.default_real @{option auto_time_start})),
+         {delay = SOME (seconds (Options.default_real @{system_option auto_time_start})),
           pri = ~ weight,
           persistent = true,
           strict = true,
@@ -128,7 +128,7 @@
             let
               val state = Toplevel.proof_of st
                 |> Proof.map_context (Context_Position.set_visible false)
-              val auto_time_limit = Options.default_real @{option auto_time_limit}
+              val auto_time_limit = Options.default_real @{system_option auto_time_limit}
             in
               if auto_time_limit > 0.0 then
                 (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of