src/Pure/PIDE/document.ML
changeset 54519 5fed81762406
parent 54516 2a7f9e79cb28
child 54526 92961f196d9e
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Nov 19 13:54:02 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Nov 19 19:33:27 2013 +0100
     1.3 @@ -18,7 +18,9 @@
     1.4    type edit = string * node_edit
     1.5    type state
     1.6    val init_state: state
     1.7 -  val define_command: Document_ID.command -> string -> string -> state -> state
     1.8 +  val define_blob: string -> string -> state -> state
     1.9 +  val define_command: Document_ID.command -> string -> Command.blob list -> string ->
    1.10 +    state -> state
    1.11    val remove_versions: Document_ID.version list -> state -> state
    1.12    val start_execution: state -> state
    1.13    val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
    1.14 @@ -231,29 +233,32 @@
    1.15  
    1.16  abstype state = State of
    1.17   {versions: version Inttab.table,  (*version id -> document content*)
    1.18 -  commands: (string * Token.T list lazy) Inttab.table,  (*command id -> named command span*)
    1.19 +  blobs: string Symtab.table,  (*digest -> text*)
    1.20 +  commands: (string * Command.blob list * Token.T list lazy) Inttab.table,
    1.21 +    (*command id -> name, inlined files, command span*)
    1.22    execution: execution}  (*current execution process*)
    1.23  with
    1.24  
    1.25 -fun make_state (versions, commands, execution) =
    1.26 -  State {versions = versions, commands = commands, execution = execution};
    1.27 +fun make_state (versions, blobs, commands, execution) =
    1.28 +  State {versions = versions, blobs = blobs, commands = commands, execution = execution};
    1.29  
    1.30 -fun map_state f (State {versions, commands, execution}) =
    1.31 -  make_state (f (versions, commands, execution));
    1.32 +fun map_state f (State {versions, blobs, commands, execution}) =
    1.33 +  make_state (f (versions, blobs, commands, execution));
    1.34  
    1.35  val init_state =
    1.36 -  make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty, no_execution);
    1.37 +  make_state (Inttab.make [(Document_ID.none, empty_version)],
    1.38 +    Symtab.empty, Inttab.empty, no_execution);
    1.39  
    1.40  
    1.41  (* document versions *)
    1.42  
    1.43  fun define_version version_id version =
    1.44 -  map_state (fn (versions, commands, {delay_request, frontier, ...}) =>
    1.45 +  map_state (fn (versions, blobs, commands, {delay_request, frontier, ...}) =>
    1.46      let
    1.47        val versions' = Inttab.update_new (version_id, version) versions
    1.48          handle Inttab.DUP dup => err_dup "document version" dup;
    1.49        val execution' = new_execution version_id delay_request frontier;
    1.50 -    in (versions', commands, execution') end);
    1.51 +    in (versions', blobs, commands, execution') end);
    1.52  
    1.53  fun the_version (State {versions, ...}) version_id =
    1.54    (case Inttab.lookup versions version_id of
    1.55 @@ -265,10 +270,23 @@
    1.56      handle Inttab.UNDEF _ => err_undef "document version" version_id;
    1.57  
    1.58  
    1.59 +(* inlined files *)
    1.60 +
    1.61 +fun define_blob digest text =
    1.62 +  map_state (fn (versions, blobs, commands, execution) =>
    1.63 +    let val blobs' = Symtab.update (digest, text) blobs
    1.64 +    in (versions, blobs', commands, execution) end);
    1.65 +
    1.66 +fun the_blob (State {blobs, ...}) digest =
    1.67 +  (case Symtab.lookup blobs digest of
    1.68 +    NONE => error ("Undefined blob: " ^ digest)
    1.69 +  | SOME text => text);
    1.70 +
    1.71 +
    1.72  (* commands *)
    1.73  
    1.74 -fun define_command command_id name text =
    1.75 -  map_state (fn (versions, commands, execution) =>
    1.76 +fun define_command command_id name command_blobs text =
    1.77 +  map_state (fn (versions, blobs, commands, execution) =>
    1.78      let
    1.79        val id = Document_ID.print command_id;
    1.80        val span =
    1.81 @@ -279,9 +297,9 @@
    1.82          Position.setmp_thread_data (Position.id_only id)
    1.83            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
    1.84        val commands' =
    1.85 -        Inttab.update_new (command_id, (name, span)) commands
    1.86 +        Inttab.update_new (command_id, (name, command_blobs, span)) commands
    1.87            handle Inttab.DUP dup => err_dup "command" dup;
    1.88 -    in (versions, commands', execution) end);
    1.89 +    in (versions, blobs, commands', execution) end);
    1.90  
    1.91  fun the_command (State {commands, ...}) command_id =
    1.92    (case Inttab.lookup commands command_id of
    1.93 @@ -295,7 +313,7 @@
    1.94  
    1.95  (* remove_versions *)
    1.96  
    1.97 -fun remove_versions version_ids state = state |> map_state (fn (versions, _, execution) =>
    1.98 +fun remove_versions version_ids state = state |> map_state (fn (versions, _, _, execution) =>
    1.99    let
   1.100      val _ =
   1.101        member (op =) version_ids (#version_id execution) andalso
   1.102 @@ -308,12 +326,17 @@
   1.103            String_Graph.fold (fn (_, (node, _)) => node |>
   1.104              iterate_entries (fn ((_, command_id), _) =>
   1.105                SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
   1.106 -  in (versions', commands', execution) end);
   1.107 +    val blobs' =
   1.108 +      (commands', Symtab.empty) |->
   1.109 +        Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
   1.110 +          fold (fn Exn.Res (_, digest) => Symtab.update (digest, the_blob state digest) | _ => I));
   1.111 +
   1.112 +  in (versions', blobs', commands', execution) end);
   1.113  
   1.114  
   1.115  (* document execution *)
   1.116  
   1.117 -fun start_execution state = state |> map_state (fn (versions, commands, execution) =>
   1.118 +fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
   1.119    timeit "Document.start_execution" (fn () =>
   1.120      let
   1.121        val {version_id, execution_id, delay_request, frontier} = execution;
   1.122 @@ -350,7 +373,7 @@
   1.123        val execution' =
   1.124          {version_id = version_id, execution_id = execution_id,
   1.125           delay_request = delay_request', frontier = frontier'};
   1.126 -    in (versions, commands, execution') end));
   1.127 +    in (versions, blobs, commands, execution') end));
   1.128  
   1.129  
   1.130  
   1.131 @@ -476,9 +499,12 @@
   1.132  
   1.133        val command_visible = visible_command node command_id';
   1.134        val command_overlays = overlays node command_id';
   1.135 -      val (command_name, span) = the_command state command_id' ||> Lazy.force;
   1.136 +      val (command_name, blobs0, span0) = the_command state command_id';
   1.137 +      val blobs = map (Exn.map_result (apsnd (the_blob state))) blobs0;
   1.138 +      val span = Lazy.force span0;
   1.139  
   1.140 -      val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
   1.141 +      val eval' =
   1.142 +        Command.eval (fn () => the_default illegal_init init span) blobs span eval;
   1.143        val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
   1.144        val exec' = (eval', prints');
   1.145