src/Pure/PIDE/document.ML

--- a/src/Pure/PIDE/document.ML	Tue Nov 19 13:54:02 2013 +0100
+++ b/src/Pure/PIDE/document.ML	Tue Nov 19 19:33:27 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 ->
@@ -231,29 +233,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 +270,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 +297,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 +313,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 +326,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 (_, digest) => Symtab.update (digest, the_blob state digest) | _ => 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 +373,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));
 
 
 
@@ -476,9 +499,12 @@
 
       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 (Exn.map_result (apsnd (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) blobs span eval;
       val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
       val exec' = (eval', prints');