# HG changeset patch
# User wenzelm
# Date 1384962189 -3600
# Node ID b2ce7a25cd8b04a61af764c2d8840189578e1af0
# Parent  4bc48d7136026cb49c7b24f47f735d6ee0f03c18# Parent  8330faaeebd59bbefaec66f1923834095aa47be9
merged

diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/General/bytes.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -89,7 +89,7 @@
 
   /* content */
 
-  def sha1_digest: SHA1.Digest = SHA1.digest(bytes)
+  lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
 
   override def toString: String =
     UTF8.decode_chars(s => s, bytes, offset, offset + length).toString
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Isar/keyword.ML	Wed Nov 20 16:43:09 2013 +0100
@@ -51,7 +51,7 @@
   val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
   val is_keyword: string -> bool
   val command_keyword: string -> T option
-  val command_files: string -> string list
+  val command_files: string -> Path.T -> Path.T list
   val command_tags: string -> string list
   val dest: unit -> string list * string list
   val define: string * T option -> unit
@@ -196,7 +196,15 @@
   in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
 
 fun command_keyword name = Symtab.lookup (get_commands ()) name;
-val command_files = these o Option.map (#2 o kind_files_of) o command_keyword;
+
+fun command_files name path =
+  (case command_keyword name of
+    NONE => []
+  | SOME (Keyword {kind, files, ...}) =>
+      if kind <> kind_of thy_load then []
+      else if null files then [path]
+      else map (fn ext => Path.ext ext path) files);
+
 val command_tags = these o Option.map tags_of o command_keyword;
 
 fun dest () = pairself (sort_strings o Scan.dest_lexicon) (get_lexicons ());
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -58,11 +58,11 @@
 
   def thy_load(span: List[Token]): Option[List[String]] =
     keywords.get(Command.name(span)) match {
-      case Some((Keyword.THY_LOAD, files)) => Some(files)
+      case Some((Keyword.THY_LOAD, exts)) => Some(exts)
       case _ => None
     }
 
-  def thy_load_commands: List[(String, List[String])] =
+  val thy_load_commands: List[(String, List[String])] =
     (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList
 
   def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Isar/token.ML	Wed Nov 20 16:43:09 2013 +0100
@@ -13,7 +13,7 @@
   type file = {src_path: Path.T, text: string, pos: Position.T}
   datatype value =
     Text of string | Typ of typ | Term of term | Fact of thm list |
-    Attribute of morphism -> attribute | Files of file list
+    Attribute of morphism -> attribute | Files of file Exn.result list
   type T
   val str_of_kind: kind -> string
   val position_of: T -> Position.T
@@ -46,8 +46,8 @@
   val content_of: T -> string
   val unparse: T -> string
   val text_of: T -> string * string
-  val get_files: T -> file list option
-  val put_files: file list -> T -> T
+  val get_files: T -> file Exn.result list
+  val put_files: file Exn.result list -> T -> T
   val get_value: T -> value option
   val map_value: (value -> value) -> T -> T
   val mk_text: string -> T
@@ -88,7 +88,7 @@
   Term of term |
   Fact of thm list |
   Attribute of morphism -> attribute |
-  Files of file list;
+  Files of file Exn.result list;
 
 datatype slot =
   Slot |
@@ -244,10 +244,11 @@
 
 (* inlined file content *)
 
-fun get_files (Token (_, _, Value (SOME (Files files)))) = SOME files
-  | get_files _ = NONE;
+fun get_files (Token (_, _, Value (SOME (Files files)))) = files
+  | get_files _ = [];
 
-fun put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
+fun put_files [] tok = tok
+  | put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
   | put_files _ tok =
       raise Fail ("Cannot put inlined files here" ^ Position.here (position_of tok));
 
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Nov 20 16:43:09 2013 +0100
@@ -6,13 +6,15 @@
 
 signature COMMAND =
 sig
-  val read: (unit -> theory) -> Token.T list -> Toplevel.transition
+  type blob = (string * string 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
   val eval_eq: eval * eval -> bool
   val eval_running: eval -> bool
   val eval_finished: eval -> bool
   val eval_result_state: eval -> Toplevel.state
-  val eval: (unit -> theory) -> Token.T list -> eval -> eval
+  val eval: (unit -> theory) -> Path.T -> blob list -> Token.T list -> eval -> eval
   type print
   val print: bool -> (string * string list) list -> string ->
     eval -> print list -> print list option
@@ -82,7 +84,38 @@
 
 (* read *)
 
-fun read init span =
+type blob = (string * string option) Exn.result;  (*file node name, digest or text*)
+
+fun read_file master_dir pos src_path =
+  let
+    val full_path = File.check_file (File.full_path master_dir src_path);
+    val _ = Position.report pos (Markup.path (Path.implode full_path));
+  in {src_path = src_path, text = File.read full_path, pos = Path.position full_path} end;
+
+fun resolve_files master_dir blobs toks =
+  (case Thy_Syntax.parse_spans toks of
+    [span] => span
+      |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
+        let
+          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, SOME text)) =
+                let val _ = Position.report pos (Markup.path file)
+                in Exn.Res {src_path = src_path, text = text, pos = Position.file file} end
+            | 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)
+          else if length src_paths = length blobs then
+            map2 make_file src_paths blobs
+          else error ("Misalignment of inlined files" ^ Position.here pos)
+        end)
+      |> Thy_Syntax.span_content
+  | _ => toks);
+
+fun read init master_dir blobs span =
   let
     val outer_syntax = #2 (Outer_Syntax.get_syntax ());
     val command_reports = Outer_Syntax.command_reports outer_syntax;
@@ -99,7 +132,7 @@
   in
     if is_malformed then Toplevel.malformed pos "Malformed command syntax"
     else
-      (case Outer_Syntax.read_spans outer_syntax span of
+      (case Outer_Syntax.read_spans outer_syntax (resolve_files master_dir blobs span) of
         [tr] =>
           if Keyword.is_control (Toplevel.name_of tr) then
             Toplevel.malformed pos "Illegal control command"
@@ -180,14 +213,14 @@
 
 in
 
-fun eval init span eval0 =
+fun eval init master_dir blobs span eval0 =
   let
     val exec_id = Document_ID.make ();
     fun process () =
       let
         val tr =
           Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
-            (fn () => read init span |> Toplevel.exec_id exec_id) ();
+            (fn () => read init master_dir blobs span |> Toplevel.exec_id exec_id) ();
       in eval_state span tr (eval_result eval0) end;
   in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
 
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -144,11 +144,13 @@
   def name(span: List[Token]): String =
     span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
 
+  type Blob = Exn.Result[(Document.Node.Name, Option[SHA1.Digest])]
+
   def apply(
     id: Document_ID.Command,
     node_name: Document.Node.Name,
+    blobs: List[Blob],
     span: List[Token],
-    thy_load: Option[List[String]],
     results: Results = Results.empty,
     markup: Markup_Tree = Markup_Tree.empty): Command =
   {
@@ -167,14 +169,14 @@
       i += n
     }
 
-    new Command(id, node_name, span1.toList, source, thy_load, results, markup)
+    new Command(id, node_name, blobs, span1.toList, source, results, markup)
   }
 
-  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, None)
+  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
 
   def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
       : Command =
-    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), None,
+    Command(id, Document.Node.Name.empty, Nil, List(Token(Token.Kind.UNPARSED, source)),
       results, markup)
 
   def unparsed(source: String): Command =
@@ -213,9 +215,9 @@
 final class Command private(
     val id: Document_ID.Command,
     val node_name: Document.Node.Name,
+    val blobs: List[Command.Blob],
     val span: List[Token],
     val source: String,
-    val thy_load: Option[List[String]],
     val init_results: Command.Results,
     val init_markup: Markup_Tree)
 {
@@ -235,6 +237,15 @@
     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
 
 
+  /* blobs */
+
+  def blobs_names: List[Document.Node.Name] =
+    for (Exn.Res((name, _)) <- blobs) yield name
+
+  def blobs_digests: List[SHA1.Digest] =
+    for (Exn.Res((_, Some(digest))) <- blobs) yield digest
+
+
   /* source */
 
   def length: Int = source.length
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/PIDE/document.ML	Wed Nov 20 16:43:09 2013 +0100
@@ -18,7 +18,9 @@
   type edit = string * node_edit
   type state
   val init_state: state
-  val define_command: Document_ID.command -> string -> string -> state -> state
+  val define_blob: string -> string -> state -> state
+  val define_command: Document_ID.command -> string -> Command.blob list -> string ->
+    state -> state
   val remove_versions: Document_ID.version list -> state -> state
   val start_execution: state -> state
   val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
@@ -70,7 +72,7 @@
   visible_last = try List.last command_ids,
   overlays = Inttab.make_list overlays};
 
-val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
+val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["No theory header"]);
 val no_perspective = make_perspective (false, [], []);
 
 val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
@@ -88,9 +90,14 @@
 
 fun read_header node span =
   let
-    val (dir, {name = (name, _), imports, keywords}) = get_header node;
+    val {name = (name, _), imports, keywords} = #2 (get_header node);
     val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
-  in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords) end;
+  in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
+
+fun master_directory node =
+  (case try Url.explode (#1 (get_header node)) of
+    SOME (Url.File path) => path
+  | _ => Path.current);
 
 fun get_perspective (Node {perspective, ...}) = perspective;
 fun set_perspective args =
@@ -231,29 +238,32 @@
 
 abstype state = State of
  {versions: version Inttab.table,  (*version id -> document content*)
-  commands: (string * Token.T list lazy) Inttab.table,  (*command id -> named command span*)
+  blobs: string Symtab.table,  (*digest -> text*)
+  commands: (string * Command.blob list * Token.T list lazy) Inttab.table,
+    (*command id -> name, inlined files, command span*)
   execution: execution}  (*current execution process*)
 with
 
-fun make_state (versions, commands, execution) =
-  State {versions = versions, commands = commands, execution = execution};
+fun make_state (versions, blobs, commands, execution) =
+  State {versions = versions, blobs = blobs, commands = commands, execution = execution};
 
-fun map_state f (State {versions, commands, execution}) =
-  make_state (f (versions, commands, execution));
+fun map_state f (State {versions, blobs, commands, execution}) =
+  make_state (f (versions, blobs, commands, execution));
 
 val init_state =
-  make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty, no_execution);
+  make_state (Inttab.make [(Document_ID.none, empty_version)],
+    Symtab.empty, Inttab.empty, no_execution);
 
 
 (* document versions *)
 
 fun define_version version_id version =
-  map_state (fn (versions, commands, {delay_request, frontier, ...}) =>
+  map_state (fn (versions, blobs, commands, {delay_request, frontier, ...}) =>
     let
       val versions' = Inttab.update_new (version_id, version) versions
         handle Inttab.DUP dup => err_dup "document version" dup;
       val execution' = new_execution version_id delay_request frontier;
-    in (versions', commands, execution') end);
+    in (versions', blobs, commands, execution') end);
 
 fun the_version (State {versions, ...}) version_id =
   (case Inttab.lookup versions version_id of
@@ -265,10 +275,23 @@
     handle Inttab.UNDEF _ => err_undef "document version" version_id;
 
 
+(* inlined files *)
+
+fun define_blob digest text =
+  map_state (fn (versions, blobs, commands, execution) =>
+    let val blobs' = Symtab.update (digest, text) blobs
+    in (versions, blobs', commands, execution) end);
+
+fun the_blob (State {blobs, ...}) digest =
+  (case Symtab.lookup blobs digest of
+    NONE => error ("Undefined blob: " ^ digest)
+  | SOME text => text);
+
+
 (* commands *)
 
-fun define_command command_id name text =
-  map_state (fn (versions, commands, execution) =>
+fun define_command command_id name command_blobs text =
+  map_state (fn (versions, blobs, commands, execution) =>
     let
       val id = Document_ID.print command_id;
       val span =
@@ -279,9 +302,9 @@
         Position.setmp_thread_data (Position.id_only id)
           (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
       val commands' =
-        Inttab.update_new (command_id, (name, span)) commands
+        Inttab.update_new (command_id, (name, command_blobs, span)) commands
           handle Inttab.DUP dup => err_dup "command" dup;
-    in (versions, commands', execution) end);
+    in (versions, blobs, commands', execution) end);
 
 fun the_command (State {commands, ...}) command_id =
   (case Inttab.lookup commands command_id of
@@ -295,7 +318,7 @@
 
 (* remove_versions *)
 
-fun remove_versions version_ids state = state |> map_state (fn (versions, _, execution) =>
+fun remove_versions version_ids state = state |> map_state (fn (versions, _, _, execution) =>
   let
     val _ =
       member (op =) version_ids (#version_id execution) andalso
@@ -308,12 +331,17 @@
           String_Graph.fold (fn (_, (node, _)) => node |>
             iterate_entries (fn ((_, command_id), _) =>
               SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
-  in (versions', commands', execution) end);
+    val blobs' =
+      (commands', Symtab.empty) |->
+        Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
+          fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
+
+  in (versions', blobs', commands', execution) end);
 
 
 (* document execution *)
 
-fun start_execution state = state |> map_state (fn (versions, commands, execution) =>
+fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
   timeit "Document.start_execution" (fn () =>
     let
       val {version_id, execution_id, delay_request, frontier} = execution;
@@ -350,7 +378,7 @@
       val execution' =
         {version_id = version_id, execution_id = execution_id,
          delay_request = delay_request', frontier = frontier'};
-    in (versions, commands, execution') end));
+    in (versions, blobs, commands, execution') end));
 
 
 
@@ -391,18 +419,19 @@
         Symtab.update (a, ())) all_visible all_required
   end;
 
+fun loaded_theory name =
+  (case try (unsuffix ".thy") name of
+    SOME a => Thy_Info.lookup_theory a
+  | NONE => NONE);
+
 fun init_theory deps node span =
   let
-    (* FIXME provide files via Isabelle/Scala, not master_dir *)
-    val (dir, header) = read_header node span;
-    val master_dir =
-      (case try Url.explode dir of
-        SOME (Url.File path) => path
-      | _ => Path.current);
+    val master_dir = master_directory node;
+    val header = read_header node span;
     val imports = #imports header;
     val parents =
       imports |> map (fn (import, _) =>
-        (case Thy_Info.lookup_theory import of
+        (case loaded_theory import of
           SOME thy => thy
         | NONE =>
             Toplevel.end_theory (Position.file_only import)
@@ -413,7 +442,7 @@
   in Thy_Load.begin_theory master_dir header parents end;
 
 fun check_theory full name node =
-  is_some (Thy_Info.lookup_theory name) orelse
+  is_some (loaded_theory name) orelse
   can get_header node andalso (not full orelse is_some (get_result node));
 
 fun last_common state node_required node0 node =
@@ -471,9 +500,13 @@
 
       val command_visible = visible_command node command_id';
       val command_overlays = overlays node command_id';
-      val (command_name, span) = the_command state command_id' ||> Lazy.force;
+      val (command_name, blobs0, span0) = the_command state command_id';
+      val blobs = (map o Exn.map_result o apsnd o Option.map) (the_blob state) blobs0;
+      val span = Lazy.force span0;
 
-      val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
+      val eval' =
+        Command.eval (fn () => the_default illegal_init init span)
+          (master_directory node) blobs span eval;
       val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
       val exec' = (eval', prints');
 
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -47,6 +47,8 @@
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
   type Edit_Command = Edit[Command.Edit, Command.Perspective]
 
+  type Blobs = Map[Node.Name, Bytes]
+
   object Node
   {
     val empty: Node = new Node()
@@ -64,9 +66,11 @@
 
     def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
 
+    val no_header = bad_header("No theory header")
+
     object Name
     {
-      val empty = Name("", "", "")
+      val empty = Name("")
 
       object Ordering extends scala.math.Ordering[Name]
       {
@@ -74,7 +78,7 @@
       }
     }
 
-    sealed case class Name(node: String, dir: String, theory: String)
+    sealed case class Name(node: String, master_dir: String = "", theory: String = "")
     {
       override def hashCode: Int = node.hashCode
       override def equals(that: Any): Boolean =
@@ -82,7 +86,9 @@
           case other: Name => node == other.node
           case _ => false
         }
-      override def toString: String = theory
+
+      def is_theory: Boolean = !theory.isEmpty
+      override def toString: String = if (is_theory) theory else node
     }
 
 
@@ -121,6 +127,7 @@
     case class Edits[A, B](edits: List[A]) extends Edit[A, B]
     case class Deps[A, B](header: Header) extends Edit[A, B]
     case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B]
+    case class Blob[A, B]() extends Edit[A, B]
     type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
     type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
 
@@ -149,7 +156,7 @@
     final class Commands private(val commands: Linear_Set[Command])
     {
       lazy val thy_load_commands: List[Command] =
-        commands.iterator.filter(_.thy_load.isDefined).toList
+        commands.iterator.filter(cmd => !cmd.blobs.isEmpty).toList
 
       private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
       {
@@ -246,6 +253,14 @@
     def entries: Iterator[(Node.Name, Node)] =
       graph.entries.map({ case (name, (node, _)) => (name, node) })
 
+    def thy_load_commands(file_name: Node.Name): List[Command] =
+      (for {
+        (_, node) <- entries
+        cmd <- node.thy_load_commands.iterator
+        name <- cmd.blobs_names.iterator
+        if name == file_name
+      } yield cmd).toList
+
     def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
     def topological_order: List[Node.Name] = graph.topological_order
   }
@@ -392,6 +407,7 @@
 
   final case class State private(
     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
     val assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
@@ -406,6 +422,9 @@
         assignments = assignments + (id -> assignment.unfinished))
     }
 
+    def define_blob(digest: SHA1.Digest): State = copy(blobs = blobs + digest)
+    def defined_blob(digest: SHA1.Digest): Boolean = blobs.contains(digest)
+
     def define_command(command: Command): State =
     {
       val id = command.id
@@ -509,6 +528,7 @@
     {
       val versions1 = versions -- removed
       val assignments1 = assignments -- removed
+      var blobs1 = Set.empty[SHA1.Digest]
       var commands1 = Map.empty[Document_ID.Command, Command.State]
       var execs1 = Map.empty[Document_ID.Exec, Command.State]
       for {
@@ -517,14 +537,19 @@
         (_, node) <- version.nodes.entries
         command <- node.commands.iterator
       } {
+        for (digest <- command.blobs_digests; if !blobs1.contains(digest))
+          blobs1 += digest
+
         if (!commands1.isDefinedAt(command.id))
           commands.get(command.id).foreach(st => commands1 += (command.id -> st))
+
         for (exec_id <- command_execs.getOrElse(command.id, Nil)) {
           if (!execs1.isDefinedAt(exec_id))
             execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
         }
       }
-      copy(versions = versions1, commands = commands1, execs = execs1, assignments = assignments1)
+      copy(versions = versions1, blobs = blobs1, commands = commands1, execs = execs1,
+        assignments = assignments1)
     }
 
     def command_state(version: Version, command: Command): Command.State =
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/PIDE/protocol.ML	Wed Nov 20 16:43:09 2013 +0100
@@ -23,9 +23,23 @@
       end);
 
 val _ =
+  Isabelle_Process.protocol_command "Document.define_blob"
+    (fn [digest, content] => Document.change_state (Document.define_blob digest content));
+
+val _ =
   Isabelle_Process.protocol_command "Document.define_command"
-    (fn [id, name, text] =>
-      Document.change_state (Document.define_command (Document_ID.parse id) name text));
+    (fn [id, name, blobs_yxml, text] =>
+      let
+        val blobs =
+          YXML.parse_body blobs_yxml |>
+            let open XML.Decode in
+              list (variant
+               [fn ([], a) => Exn.Res (pair string (option string) a),
+                fn ([], a) => Exn.Exn (ERROR (string a))])
+            end;
+      in
+        Document.change_state (Document.define_command (Document_ID.parse id) name blobs text)
+      end);
 
 val _ =
   Isabelle_Process.protocol_command "Document.discontinue_execution"
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -308,11 +308,28 @@
 
 trait Protocol extends Isabelle_Process
 {
+  /* inlined files */
+
+  def define_blob(blob: Bytes): Unit =
+    protocol_command_raw("Document.define_blob", Bytes(blob.sha1_digest.toString), blob)
+
+
   /* commands */
 
   def define_command(command: Command): Unit =
+  {
+    val blobs_yxml =
+    { import XML.Encode._
+      val encode_blob: T[Command.Blob] =
+        variant(List(
+          { case Exn.Res((a, b)) =>
+              (Nil, pair(string, option(string))((a.node, b.map(_.toString)))) },
+          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
+      YXML.string_of_body(list(encode_blob)(command.blobs))
+    }
     protocol_command("Document.define_command",
-      Document_ID(command.id), encode(command.name), encode(command.source))
+      Document_ID(command.id), encode(command.name), blobs_yxml, encode(command.source))
+  }
 
 
   /* execution */
@@ -335,10 +352,11 @@
       def encode_edit(name: Document.Node.Name)
           : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
         variant(List(
+          // FIXME Document.Node.Blob (!??)
           { case Document.Node.Clear() => (Nil, Nil) },  // FIXME unused !?
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
           { case Document.Node.Deps(header) =>
-              val dir = Isabelle_System.posix_path(name.dir)
+              val master_dir = Isabelle_System.posix_path(name.master_dir)
               val imports = header.imports.map(_.node)
               val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
               (Nil,
@@ -346,7 +364,7 @@
                   pair(list(pair(Encode.string,
                     option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
                   list(Encode.string)))))(
-                (dir, (name.theory, (imports, (keywords, header.errors)))))) },
+                (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
           { case Document.Node.Perspective(a, b, c) =>
               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
                 list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/System/session.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -25,7 +25,7 @@
   case class Statistics(props: Properties.T)
   case class Global_Options(options: Options)
   case object Caret_Focus
-  case class Raw_Edits(edits: List[Document.Edit_Text])
+  case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
@@ -167,6 +167,7 @@
   //{{{
   private case class Text_Edits(
     previous: Future[Document.Version],
+    doc_blobs: Document.Blobs,
     text_edits: List[Document.Edit_Text],
     version_result: Promise[Document.Version])
 
@@ -177,14 +178,14 @@
       receive {
         case Stop => finished = true; reply(())
 
-        case Text_Edits(previous, text_edits, version_result) =>
+        case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
           val prev = previous.get_finished
           val (doc_edits, version) =
             Timing.timeit("Thy_Load.text_edits", timing) {
-              thy_load.text_edits(reparse_limit, prev, text_edits)
+              thy_load.text_edits(reparse_limit, prev, doc_blobs, text_edits)
             }
           version_result.fulfill(version)
-          sender ! Change(doc_edits, prev, version)
+          sender ! Change(doc_blobs, doc_edits, prev, version)
 
         case bad => System.err.println("change_parser: ignoring bad message " + bad)
       }
@@ -250,6 +251,7 @@
   private case class Start(args: List[String])
   private case class Cancel_Exec(exec_id: Document_ID.Exec)
   private case class Change(
+    doc_blobs: Document.Blobs,
     doc_edits: List[Document.Edit_Command],
     previous: Document.Version,
     version: Document.Version)
@@ -348,7 +350,7 @@
 
     /* raw edits */
 
-    def handle_raw_edits(edits: List[Document.Edit_Text])
+    def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
     //{{{
     {
       prover.get.discontinue_execution()
@@ -357,8 +359,8 @@
       val version = Future.promise[Document.Version]
       val change = global_state >>> (_.continue_history(previous, edits, version))
 
-      raw_edits.event(Session.Raw_Edits(edits))
-      change_parser ! Text_Edits(previous, edits, version)
+      raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
+      change_parser ! Text_Edits(previous, doc_blobs, edits, version)
     }
     //}}}
 
@@ -374,6 +376,18 @@
 
       def id_command(command: Command)
       {
+        for {
+          digest <- command.blobs_digests
+          if !global_state().defined_blob(digest)
+        } {
+          change.doc_blobs.collectFirst({ case (_, b) if b.sha1_digest == digest => b }) match {
+            case Some(blob) =>
+              global_state >> (_.define_blob(digest))
+              prover.get.define_blob(blob)
+            case None => System.err.println("Missing blob for SHA1 digest " + digest)
+          }
+        }
+
         if (!global_state().defined_command(command.id)) {
           global_state >> (_.define_command(command))
           prover.get.define_command(command)
@@ -510,7 +524,7 @@
         case Update_Options(options) if prover.isDefined =>
           if (is_ready) {
             prover.get.options(options)
-            handle_raw_edits(Nil)
+            handle_raw_edits(Map.empty, Nil)
           }
           global_options.event(Session.Global_Options(options))
           reply(())
@@ -518,8 +532,8 @@
         case Cancel_Exec(exec_id) if prover.isDefined =>
           prover.get.cancel_exec(exec_id)
 
-        case Session.Raw_Edits(edits) if prover.isDefined =>
-          handle_raw_edits(edits)
+        case Session.Raw_Edits(doc_blobs, edits) if prover.isDefined =>
+          handle_raw_edits(doc_blobs, edits)
           reply(())
 
         case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
@@ -572,8 +586,8 @@
 
   def cancel_exec(exec_id: Document_ID.Exec) { session_actor ! Cancel_Exec(exec_id) }
 
-  def update(edits: List[Document.Edit_Text])
-  { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(edits) }
+  def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
+  { if (!edits.isEmpty) session_actor !? Session.Raw_Edits(doc_blobs, edits) }
 
   def update_options(options: Options)
   { session_actor !? Update_Options(options) }
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Thy/thy_info.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -68,7 +68,7 @@
       val dep_files =
         rev_deps.par.map(dep =>
           Exn.capture {
-            dep.load_files(syntax).map(a => Path.explode(dep.name.dir) + Path.explode(a))
+            dep.load_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
           }).toList
       ((Nil: List[Path]) /: dep_files) {
         case (acc_files, files) => Exn.release(files) ::: acc_files
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Wed Nov 20 16:43:09 2013 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Thy/thy_load.ML
     Author:     Makarius
 
-Loading files that contribute to a theory.
+Management of theory sources and auxiliary files.
 *)
 
 signature THY_LOAD =
@@ -9,11 +9,10 @@
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val thy_path: Path.T -> Path.T
-  val read_files: Path.T -> string -> Path.T * Position.T -> Token.file list
-  val parse_files: string -> (theory -> Token.file list) parser
   val check_thy: Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
     imports: (string * Position.T) list, keywords: Thy_Header.keywords}
+  val parse_files: string -> (theory -> Token.file list) parser
   val provide: Path.T * SHA1.digest -> theory -> theory
   val provide_parse_files: string -> (theory -> Token.file list * theory) parser
   val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
@@ -56,34 +55,12 @@
 fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
 
 
-(* auxiliary files *)
-
-fun check_file dir file = File.check_file (File.full_path dir file);
-
-fun read_files dir cmd (path, pos) =
-  let
-    fun make_file file =
-      let
-        val _ = Position.report pos (Markup.path (Path.implode file));
-        val full_path = check_file dir file;
-      in {src_path = file, text = File.read full_path, pos = Path.position full_path} end;
-    val paths =
-      (case Keyword.command_files cmd of
-        [] => [path]
-      | exts => map (fn ext => Path.ext ext path) exts);
-  in map make_file paths end;
-
-fun parse_files cmd =
-  Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
-    (case Token.get_files tok of
-      SOME files => files
-    | NONE => read_files (master_directory thy) cmd (Path.explode name, Token.position_of tok)));
-
-
 (* theory files *)
 
 val thy_path = Path.ext "thy";
 
+fun check_file dir file = File.check_file (File.full_path dir file);
+
 fun check_thy dir thy_name =
   let
     val path = thy_path (Path.basic thy_name);
@@ -102,6 +79,17 @@
 
 (* load files *)
 
+fun parse_files cmd =
+  Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
+    (case Token.get_files tok of
+      [] =>
+        let
+          val master_dir = master_directory thy;
+          val pos = Token.position_of tok;
+          val src_paths = Keyword.command_files cmd (Path.explode name);
+        in map (Command.read_file master_dir pos) src_paths end
+    | files => map Exn.release files));
+
 fun provide (src_path, id) =
   map_files (fn (master_dir, imports, provided) =>
     if AList.defined (op =) provided src_path then
@@ -135,18 +123,18 @@
   in map (File.full_path master_dir o #1) provided end;
 
 
-(* load_thy *)
+(* load theory *)
 
 fun begin_theory master_dir {name, imports, keywords} parents =
   Theory.begin_theory name parents
   |> put_deps master_dir imports
   |> fold Thy_Header.declare_keyword keywords;
 
-fun excursion last_timing init elements =
+fun excursion master_dir last_timing init elements =
   let
     fun prepare_span span =
       Thy_Syntax.span_content span
-      |> Command.read init
+      |> Command.read init master_dir []
       |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
 
     fun element_result span_elem (st, _) =
@@ -171,7 +159,7 @@
 
     val lexs = Keyword.get_lexicons ();
     val toks = Thy_Syntax.parse_tokens lexs text_pos text;
-    val spans = map (Thy_Syntax.resolve_files (read_files master_dir)) (Thy_Syntax.parse_spans toks);
+    val spans = Thy_Syntax.parse_spans toks;
     val elements = Thy_Syntax.parse_elements spans;
 
     fun init () =
@@ -180,7 +168,8 @@
           (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
 
     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
-    val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements);
+    val (results, thy) =
+      cond_timeit time "" (fn () => excursion master_dir last_timing init elements);
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
 
     fun present () =
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Thy/thy_load.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -21,23 +21,23 @@
   def is_ok(str: String): Boolean =
     try { thy_path(Path.explode(str)); true }
     catch { case ERROR(_) => false }
-
-
-  /* document node names */
-
-  def path_node_name(raw_path: Path): Document.Node.Name =
-  {
-    val path = raw_path.expand
-    val node = path.implode
-    val dir = path.dir.implode
-    val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
-    Document.Node.Name(node, dir, theory)
-  }
 }
 
 
 class Thy_Load(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
 {
+  /* document node names */
+
+  def node_name(raw_path: Path): Document.Node.Name =
+  {
+    val path = raw_path.expand
+    val node = path.implode
+    val theory = Thy_Header.thy_name(node).getOrElse("")
+    val master_dir = if (theory == "") "" else path.dir.implode
+    Document.Node.Name(node, master_dir, theory)
+  }
+
+
   /* file-system operations */
 
   def append(dir: String, source_path: Path): String =
@@ -56,50 +56,24 @@
 
   /* theory files */
 
-  private def find_file(tokens: List[Token]): Option[String] =
-  {
-    def clean(toks: List[Token]): List[Token] =
-      toks match {
-        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
-        case t :: ts => t :: clean(ts)
-        case Nil => Nil
-      }
-    val clean_tokens = clean(tokens.filter(_.is_proper))
-    clean_tokens.reverse.find(_.is_name).map(_.content)
-  }
-
   def body_files_test(syntax: Outer_Syntax, text: String): Boolean =
     syntax.thy_load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
 
   def body_files(syntax: Outer_Syntax, text: String): List[String] =
   {
-    val thy_load_commands = syntax.thy_load_commands
     val spans = Thy_Syntax.parse_spans(syntax.scan(text))
-    spans.iterator.map({
-      case toks @ (tok :: _) if tok.is_command =>
-        thy_load_commands.find({ case (cmd, _) => cmd == tok.content }) match {
-          case Some((_, exts)) =>
-            find_file(toks) match {
-              case Some(file) =>
-                if (exts.isEmpty) List(file)
-                else exts.map(ext => file + "." + ext)
-              case None => Nil
-            }
-          case None => Nil
-        }
-      case _ => Nil
-    }).flatten.toList
+    spans.iterator.map(Thy_Syntax.span_files(syntax, _)).flatten.toList
   }
 
   def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
   {
     val theory = Thy_Header.base_name(s)
-    if (loaded_theories(theory)) Document.Node.Name(theory, "", theory)
+    if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory)
     else {
       val path = Path.explode(s)
-      val node = append(master.dir, Thy_Load.thy_path(path))
-      val dir = append(master.dir, path.dir)
-      Document.Node.Name(node, dir, theory)
+      val node = append(master.master_dir, Thy_Load.thy_path(path))
+      val master_dir = append(master.master_dir, path.dir)
+      Document.Node.Name(node, master_dir, theory)
     }
   }
 
@@ -125,8 +99,11 @@
 
   /* theory text edits */
 
-  def text_edits(reparse_limit: Int, previous: Document.Version, edits: List[Document.Edit_Text])
-      : (List[Document.Edit_Command], Document.Version) =
-    Thy_Syntax.text_edits(base_syntax, reparse_limit, previous, edits)
+  def text_edits(
+    reparse_limit: Int,
+    previous: Document.Version,
+    doc_blobs: Document.Blobs,
+    edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
+    Thy_Syntax.text_edits(this, reparse_limit, previous, doc_blobs, edits)
 }
 
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Wed Nov 20 16:43:09 2013 +0100
@@ -15,7 +15,7 @@
   val span_content: span -> Token.T list
   val present_span: span -> Output.output
   val parse_spans: Token.T list -> span list
-  val resolve_files: (string -> Path.T * Position.T -> Token.file list) -> span -> span
+  val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span
   datatype 'a element = Element of 'a * ('a element list * 'a) option
   val atom: 'a -> 'a element
   val map_element: ('a -> 'b) -> 'a element -> 'b element
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -33,7 +33,7 @@
 
       def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
       var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
-        List((0, node_name.theory, buffer()))
+        List((0, node_name.toString, buffer()))
 
       @tailrec def close(level: Int => Boolean)
       {
@@ -68,7 +68,7 @@
       /* result structure */
 
       val spans = parse_spans(syntax.scan(text))
-      spans.foreach(span => add(Command(Document_ID.none, node_name, span, syntax.thy_load(span))))
+      spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
       result()
     }
   }
@@ -225,23 +225,73 @@
   }
 
 
+  /* inlined files */
+
+  private def find_file(tokens: List[Token]): Option[String] =
+  {
+    def clean(toks: List[Token]): List[Token] =
+      toks match {
+        case t :: _ :: ts if t.is_keyword && (t.source == "%" || t.source == "--") => clean(ts)
+        case t :: ts => t :: clean(ts)
+        case Nil => Nil
+      }
+    val clean_tokens = clean(tokens.filter(_.is_proper))
+    clean_tokens.reverse.find(_.is_name).map(_.content)
+  }
+
+  def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] =
+    syntax.thy_load(span) match {
+      case Some(exts) =>
+        find_file(span) match {
+          case Some(file) =>
+            if (exts.isEmpty) List(file)
+            else exts.map(ext => file + "." + ext)
+          case None => Nil
+        }
+      case None => Nil
+    }
+
+  def resolve_files(
+      thy_load: Thy_Load,
+      syntax: Outer_Syntax,
+      node_name: Document.Node.Name,
+      span: List[Token],
+      doc_blobs: Document.Blobs)
+    : List[Command.Blob] =
+  {
+    span_files(syntax, span).map(file =>
+      Exn.capture {
+        val name =
+          Document.Node.Name(thy_load.append(node_name.master_dir, Path.explode(file)))
+        (name, doc_blobs.get(name).map(_.sha1_digest))
+      }
+    )
+  }
+
+
   /* reparse range of command spans */
 
   @tailrec private def chop_common(
-      cmds: List[Command], spans: List[List[Token]]): (List[Command], List[List[Token]]) =
+      cmds: List[Command], spans: List[(List[Command.Blob], List[Token])])
+      : (List[Command], List[(List[Command.Blob], List[Token])]) =
     (cmds, spans) match {
-      case (c :: cs, s :: ss) if c.span == s => chop_common(cs, ss)
+      case (c :: cs, (blobs, span) :: ps) if c.blobs == blobs && c.span == span =>
+        chop_common(cs, ps)
       case _ => (cmds, spans)
     }
 
   private def reparse_spans(
+    thy_load: Thy_Load,
     syntax: Outer_Syntax,
+    doc_blobs: Document.Blobs,
     name: Document.Node.Name,
     commands: Linear_Set[Command],
     first: Command, last: Command): Linear_Set[Command] =
   {
     val cmds0 = commands.iterator(first, last).toList
-    val spans0 = parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString))
+    val spans0 =
+      parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
+        map(span => (resolve_files(thy_load, syntax, name, span, doc_blobs), span))
 
     val (cmds1, spans1) = chop_common(cmds0, spans0)
 
@@ -256,7 +306,7 @@
       case cmd :: _ =>
         val hook = commands.prev(cmd)
         val inserted =
-          spans2.map(span => Command(Document_ID.make(), name, span, syntax.thy_load(span)))
+          spans2.map({ case (blobs, span) => Command(Document_ID.make(), name, blobs, span) })
         (commands /: cmds2)(_ - _).append_after(hook, inserted)
     }
   }
@@ -266,7 +316,9 @@
 
   // FIXME somewhat slow
   private def recover_spans(
+    thy_load: Thy_Load,
     syntax: Outer_Syntax,
+    doc_blobs: Document.Blobs,
     name: Document.Node.Name,
     perspective: Command.Perspective,
     commands: Linear_Set[Command]): Linear_Set[Command] =
@@ -282,7 +334,7 @@
         case Some(first_unparsed) =>
           val first = next_invisible_command(cmds.reverse, first_unparsed)
           val last = next_invisible_command(cmds, first_unparsed)
-          recover(reparse_spans(syntax, name, cmds, first, last))
+          recover(reparse_spans(thy_load, syntax, doc_blobs, name, cmds, first, last))
         case None => cmds
       }
     recover(commands)
@@ -292,7 +344,9 @@
   /* consolidate unfinished spans */
 
   private def consolidate_spans(
+    thy_load: Thy_Load,
     syntax: Outer_Syntax,
+    doc_blobs: Document.Blobs,
     reparse_limit: Int,
     name: Document.Node.Name,
     perspective: Command.Perspective,
@@ -312,7 +366,7 @@
                 last = it.next
                 i += last.length
               }
-              reparse_spans(syntax, name, commands, first_unfinished, last)
+              reparse_spans(thy_load, syntax, doc_blobs, name, commands, first_unfinished, last)
             case None => commands
           }
         case None => commands
@@ -333,7 +387,11 @@
     inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
   }
 
-  private def text_edit(syntax: Outer_Syntax, reparse_limit: Int,
+  private def text_edit(
+    thy_load: Thy_Load,
+    syntax: Outer_Syntax,
+    doc_blobs: Document.Blobs,
+    reparse_limit: Int,
     node: Document.Node, edit: Document.Edit_Text): Document.Node =
   {
     edit match {
@@ -342,7 +400,8 @@
       case (name, Document.Node.Edits(text_edits)) =>
         val commands0 = node.commands
         val commands1 = edit_text(text_edits, commands0)
-        val commands2 = recover_spans(syntax, name, node.perspective.visible, commands1)
+        val commands2 =
+          recover_spans(thy_load, syntax, doc_blobs, name, node.perspective.visible, commands1)
         node.update_commands(commands2)
 
       case (_, Document.Node.Deps(_)) => node
@@ -354,46 +413,64 @@
         if (node.same_perspective(perspective)) node
         else
           node.update_perspective(perspective).update_commands(
-            consolidate_spans(syntax, reparse_limit, name, visible, node.commands))
+            consolidate_spans(thy_load, syntax, doc_blobs, reparse_limit,
+              name, visible, node.commands))
+
+      case (_, Document.Node.Blob()) => node
     }
   }
 
   def text_edits(
-      base_syntax: Outer_Syntax,
+      thy_load: Thy_Load,
       reparse_limit: Int,
       previous: Document.Version,
+      doc_blobs: Document.Blobs,
       edits: List[Document.Edit_Text])
     : (List[Document.Edit_Command], Document.Version) =
   {
-    val (syntax, reparse, nodes0, doc_edits0) = header_edits(base_syntax, previous, edits)
-    val reparse_set = reparse.toSet
-
-    var nodes = nodes0
-    val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
+    val (syntax, reparse0, nodes0, doc_edits0) =
+      header_edits(thy_load.base_syntax, previous, edits)
 
-    val node_edits =
-      (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
-        .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
+    if (edits.isEmpty)
+      (Nil, Document.Version.make(syntax, previous.nodes))
+    else {
+      val reparse =
+        (reparse0 /: nodes0.entries)({
+          case (reparse, (name, node)) =>
+            if (node.thy_load_commands.isEmpty) reparse
+            else name :: reparse
+          })
+      val reparse_set = reparse.toSet
 
-    node_edits foreach {
-      case (name, edits) =>
-        val node = nodes(name)
-        val commands = node.commands
+      var nodes = nodes0
+      val doc_edits = new mutable.ListBuffer[Document.Edit_Command]; doc_edits ++= doc_edits0
+
+      val node_edits =
+        (edits ::: reparse.map((_, Document.Node.Edits(Nil)))).groupBy(_._1)
+          .asInstanceOf[Map[Document.Node.Name, List[Document.Edit_Text]]]  // FIXME ???
 
-        val node1 =
-          if (reparse_set(name) && !commands.isEmpty)
-            node.update_commands(reparse_spans(syntax, name, commands, commands.head, commands.last))
-          else node
-        val node2 = (node1 /: edits)(text_edit(syntax, reparse_limit, _, _))
+      node_edits foreach {
+        case (name, edits) =>
+          val node = nodes(name)
+          val commands = node.commands
 
-        if (!(node.same_perspective(node2.perspective)))
-          doc_edits += (name -> node2.perspective)
-
-        doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
+          val node1 =
+            if (reparse_set(name) && !commands.isEmpty)
+              node.update_commands(
+                reparse_spans(thy_load, syntax, doc_blobs,
+                  name, commands, commands.head, commands.last))
+            else node
+          val node2 = (node1 /: edits)(text_edit(thy_load, syntax, doc_blobs, reparse_limit, _, _))
 
-        nodes += (name -> node2)
+          if (!(node.same_perspective(node2.perspective)))
+            doc_edits += (name -> node2.perspective)
+
+          doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node2.commands)))
+
+          nodes += (name -> node2)
+      }
+
+      (doc_edits.toList, Document.Version.make(syntax, nodes))
     }
-
-    (doc_edits.toList, Document.Version.make(syntax, nodes))
   }
 }
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Pure/Tools/build.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -417,7 +417,8 @@
                 val parent = deps(parent_name)
                 (parent.loaded_theories, parent.syntax)
             }
-          val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
+          val thy_load = new Thy_Load(preloaded, parent_syntax)
+          val thy_info = new Thy_Info(thy_load)
 
           if (verbose || list_files) {
             val groups =
@@ -429,7 +430,7 @@
           val thy_deps =
             thy_info.dependencies(
               info.theories.map(_._2).flatten.
-                map(thy => Thy_Load.path_node_name(info.dir + Thy_Load.thy_path(thy))))
+                map(thy => thy_load.node_name(info.dir + Thy_Load.thy_path(thy))))
 
           val loaded_theories = thy_deps.loaded_theories
           val keywords = thy_deps.keywords
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -60,17 +60,23 @@
 {
   /* header */
 
+  def is_theory: Boolean = node_name.is_theory
+
   def node_header(): Document.Node.Header =
   {
     Swing_Thread.require()
-    JEdit_Lib.buffer_lock(buffer) {
-      Exn.capture {
-        PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
-      } match {
-        case Exn.Res(header) => header
-        case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
+
+    if (is_theory) {
+      JEdit_Lib.buffer_lock(buffer) {
+        Exn.capture {
+          PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
+        } match {
+          case Exn.Res(header) => header
+          case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
+        }
       }
     }
+    else Document.Node.no_header
   }
 
 
@@ -82,7 +88,7 @@
   def node_required_=(b: Boolean)
   {
     Swing_Thread.require()
-    if (_node_required != b) {
+    if (_node_required != b && is_theory) {
       _node_required = b
       PIDE.options_changed()
       PIDE.editor.flush()
@@ -96,18 +102,51 @@
   {
     Swing_Thread.require()
 
-    if (Isabelle.continuous_checking) {
+    if (Isabelle.continuous_checking && is_theory) {
       val snapshot = this.snapshot()
-      Document.Node.Perspective(node_required, Text.Perspective(
+
+      val document_view_ranges =
         for {
           doc_view <- PIDE.document_views(buffer)
           range <- doc_view.perspective(snapshot).ranges
-        } yield range), PIDE.editor.node_overlays(node_name))
+        } yield range
+
+      val thy_load_ranges =
+        for {
+          cmd <- snapshot.node.thy_load_commands
+          blob_name <- cmd.blobs_names
+          blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node)
+          if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
+          start <- snapshot.node.command_start(cmd)
+          range = snapshot.convert(cmd.proper_range + start)
+        } yield range
+
+      Document.Node.Perspective(node_required,
+        Text.Perspective(document_view_ranges ::: thy_load_ranges),
+        PIDE.editor.node_overlays(node_name))
     }
     else empty_perspective
   }
 
 
+  /* blob */
+
+  private var _blob: Option[Bytes] = None  // owned by Swing thread
+
+  private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
+
+  def blob(): Bytes =
+    Swing_Thread.require {
+      _blob match {
+        case Some(b) => b
+        case None =>
+          val b = PIDE.thy_load.file_content(buffer)
+          _blob = Some(b)
+          b
+      }
+    }
+
+
   /* edits */
 
   def init_edits(): List[Document.Edit_Text] =
@@ -118,10 +157,13 @@
     val text = JEdit_Lib.buffer_text(buffer)
     val perspective = node_perspective()
 
-    List(session.header_edit(node_name, header),
-      node_name -> Document.Node.Clear(),
-      node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
-      node_name -> perspective)
+    if (is_theory)
+      List(session.header_edit(node_name, header),
+        node_name -> Document.Node.Clear(),
+        node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
+        node_name -> perspective)
+    else
+      List(node_name -> Document.Node.Blob())
   }
 
   def node_edits(
@@ -131,16 +173,20 @@
   {
     Swing_Thread.require()
 
-    val header_edit = session.header_edit(node_name, node_header())
-    if (clear)
-      List(header_edit,
-        node_name -> Document.Node.Clear(),
-        node_name -> Document.Node.Edits(text_edits),
-        node_name -> perspective)
+    if (is_theory) {
+      val header_edit = session.header_edit(node_name, node_header())
+      if (clear)
+        List(header_edit,
+          node_name -> Document.Node.Clear(),
+          node_name -> Document.Node.Edits(text_edits),
+          node_name -> perspective)
+      else
+        List(header_edit,
+          node_name -> Document.Node.Edits(text_edits),
+          node_name -> perspective)
+    }
     else
-      List(header_edit,
-        node_name -> Document.Node.Edits(text_edits),
-        node_name -> perspective)
+      List(node_name -> Document.Node.Blob())
   }
 
 
@@ -170,6 +216,8 @@
 
     def edit(clear: Boolean, e: Text.Edit)
     {
+      reset_blob()
+
       if (clear) {
         pending_clear = true
         pending.clear
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -82,7 +82,7 @@
         PIDE.editor.current_command(view, snapshot) match {
           case Some(command) =>
             snapshot.node.command_start(command) match {
-              case Some(start) => List(command.proper_range + start)
+              case Some(start) => List(snapshot.convert(command.proper_range + start))
               case None => Nil
             }
           case None => Nil
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -133,15 +133,15 @@
 
 
 class Isabelle_Sidekick_Default extends
-  Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.buffer_node_name)
+  Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.theory_node_name)
 
 
 class Isabelle_Sidekick_Options extends
-  Isabelle_Sidekick_Structure("isabelle-options", PIDE.thy_load.buffer_node_dummy)
+  Isabelle_Sidekick_Structure("isabelle-options", _ => Some(Document.Node.Name("options")))
 
 
 class Isabelle_Sidekick_Root extends
-  Isabelle_Sidekick_Structure("isabelle-root", PIDE.thy_load.buffer_node_dummy)
+  Isabelle_Sidekick_Structure("isabelle-root", _ => Some(Document.Node.Name("ROOT")))
 
 
 class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -23,17 +23,8 @@
   {
     Swing_Thread.require()
 
-    session.update(
-      (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
-        case (edits, buffer) =>
-          JEdit_Lib.buffer_lock(buffer) {
-            PIDE.document_model(buffer) match {
-              case Some(model) => model.flushed_edits() ::: edits
-              case None => edits
-            }
-          }
-      }
-    )
+    val edits = PIDE.document_models().flatMap(_.flushed_edits())
+    if (!edits.isEmpty) session.update(PIDE.document_blobs(), edits)
   }
 
   private val delay_flush =
@@ -72,11 +63,13 @@
     Swing_Thread.require()
 
     val text_area = view.getTextArea
+    val buffer = view.getBuffer
+
     PIDE.document_view(text_area) match {
       case Some(doc_view) =>
         val node = snapshot.version.nodes(doc_view.model.node_name)
         val caret = snapshot.revert(text_area.getCaretPosition)
-        if (caret < text_area.getBuffer.getLength) {
+        if (caret < buffer.getLength) {
           val caret_commands = node.command_range(caret)
           if (caret_commands.hasNext) {
             val (cmd0, _) = caret_commands.next
@@ -85,7 +78,15 @@
           else None
         }
         else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
-      case None => None
+      case None =>
+        PIDE.document_model(buffer) match {
+          case Some(model) if !model.is_theory =>
+            snapshot.version.nodes.thy_load_commands(model.node_name) match {
+              case cmd :: _ => Some(cmd)
+              case Nil => None
+            }
+          case _ => None
+        }
     }
   }
 
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Tools/jEdit/src/jedit_thy_load.scala
--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -9,26 +9,31 @@
 
 import isabelle._
 
-import java.io.{File => JFile, IOException}
+import java.io.{File => JFile, IOException, ByteArrayOutputStream}
 import javax.swing.text.Segment
 
 import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
 import org.gjt.sp.jedit.MiscUtilities
 import org.gjt.sp.jedit.{View, Buffer}
-
+import org.gjt.sp.jedit.bufferio.BufferIORequest
 
 class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
   extends Thy_Load(loaded_theories, base_syntax)
 {
   /* document node names */
 
-  def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
-    Some(Document.Node.Name(JEdit_Lib.buffer_name(buffer), buffer.getDirectory, buffer.getName))
+  def node_name(buffer: Buffer): Document.Node.Name =
+  {
+    val node = JEdit_Lib.buffer_name(buffer)
+    val theory = Thy_Header.thy_name(node).getOrElse("")
+    val master_dir = if (theory == "") "" else buffer.getDirectory
+    Document.Node.Name(node, master_dir, theory)
+  }
 
-  def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
+  def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
   {
-    val name = JEdit_Lib.buffer_name(buffer)
-    Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
+    val name = node_name(buffer)
+    if (name.is_theory) Some(name) else None
   }
 
 
@@ -37,7 +42,7 @@
   override def append(dir: String, source_path: Path): String =
   {
     val path = source_path.expand
-    if (path.is_absolute) Isabelle_System.platform_path(path)
+    if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path)
     else {
       val vfs = VFSManager.getVFSForPath(dir)
       if (vfs.isInstanceOf[FileVFS])
@@ -83,5 +88,28 @@
       catch { case _: IOException => }
     }
   }
+
+
+  /* file content */
+
+  def file_content(buffer: Buffer): Bytes =
+  {
+    val path = buffer.getPath
+    val vfs = VFSManager.getVFSForPath(path)
+    val content =
+      new BufferIORequest(null, buffer, null, vfs, path) {
+        def _run() { }
+        def apply(): Bytes =
+        {
+          val out =
+            new ByteArrayOutputStream(buffer.getLength + 1) {
+              def content(): Bytes = Bytes(this.buf, 0, this.count)
+            }
+          write(buffer, out)
+          out.content()
+        }
+      }
+    content()
+  }
 }
 
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -73,9 +73,17 @@
   def document_views(buffer: Buffer): List[Document_View] =
     for {
       text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
-      doc_view = document_view(text_area)
-      if doc_view.isDefined
-    } yield doc_view.get
+      doc_view <- document_view(text_area)
+    } yield doc_view
+
+  def document_models(): List[Document_Model] =
+    for {
+      buffer <- JEdit_Lib.jedit_buffers().toList
+      model <- document_model(buffer)
+    } yield model
+
+  def document_blobs(): Document.Blobs =
+    document_models().filterNot(_.is_theory).map(model => (model.node_name -> model.blob())).toMap
 
   def exit_models(buffers: List[Buffer])
   {
@@ -96,27 +104,24 @@
       val init_edits =
         (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) =>
           JEdit_Lib.buffer_lock(buffer) {
-            val (model_edits, opt_model) =
-              thy_load.buffer_node_name(buffer) match {
-                case Some(node_name) =>
-                  document_model(buffer) match {
-                    case Some(model) if model.node_name == node_name => (Nil, Some(model))
-                    case _ =>
-                      val model = Document_Model.init(session, buffer, node_name)
-                      (model.init_edits(), Some(model))
-                  }
-                case None => (Nil, None)
+            val node_name = thy_load.node_name(buffer)
+            val (model_edits, model) =
+              document_model(buffer) match {
+                case Some(model) if model.node_name == node_name => (Nil, model)
+                case _ =>
+                  val model = Document_Model.init(session, buffer, node_name)
+                  (model.init_edits(), model)
               }
-            if (opt_model.isDefined) {
+            if (model.is_theory) {
               for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
-                if (document_view(text_area).map(_.model) != opt_model)
-                  Document_View.init(opt_model.get, text_area)
+                if (document_view(text_area).map(_.model) != Some(model))
+                  Document_View.init(model, text_area)
               }
             }
             model_edits ::: edits
           }
         }
-      session.update(init_edits)
+      session.update(document_blobs(), init_edits)
     }
   }
 
@@ -124,8 +129,8 @@
   {
     JEdit_Lib.swing_buffer_lock(buffer) {
       document_model(buffer) match {
-        case Some(model) => Document_View.init(model, text_area)
-        case None =>
+        case Some(model) if model.is_theory => Document_View.init(model, text_area)
+        case _ =>
       }
     }
   }
@@ -163,8 +168,11 @@
             buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
 
           val thys =
-            for (buffer <- buffers; model <- PIDE.document_model(buffer))
-              yield model.node_name
+            for {
+              buffer <- buffers
+              model <- PIDE.document_model(buffer)
+              if model.is_theory
+            } yield model.node_name
 
           val thy_info = new Thy_Info(PIDE.thy_load)
           // FIXME avoid I/O in Swing thread!?!
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -226,7 +226,7 @@
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
           if Path.is_ok(name) =>
-            val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
+            val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
             val link = PIDE.editor.hyperlink_file(jedit_file)
             Some(Text.Info(snapshot.convert(info_range), link) :: links)
 
@@ -369,7 +369,7 @@
             Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
           if Path.is_ok(name) =>
-            val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
+            val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
             Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
           if name == Markup.SORTING || name == Markup.TYPING =>
diff -r 4bc48d713602 -r b2ce7a25cd8b src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Nov 20 08:56:54 2013 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Nov 20 16:43:09 2013 +0100
@@ -186,10 +186,10 @@
     val snapshot = PIDE.session.snapshot()
 
     val iterator =
-      restriction match {
+      (restriction match {
         case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
         case None => snapshot.version.nodes.entries
-      }
+      }).filter(_._1.is_theory)
     val nodes_status1 =
       (nodes_status /: iterator)({ case (status, (name, node)) =>
           if (PIDE.thy_load.loaded_theories(name.theory)) status