src/Pure/PIDE/document.ML
changeset 59689 7968c57ea240
parent 59687 3baf9b3a24c7
child 59702 58dfaa369c11
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Mar 13 12:44:16 2015 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Mar 13 12:58:49 2015 +0100
     1.3 @@ -307,8 +307,8 @@
     1.4  abstype state = State of
     1.5   {versions: version Inttab.table,  (*version id -> document content*)
     1.6    blobs: (SHA1.digest * string list) Symtab.table,  (*raw digest -> digest, lines*)
     1.7 -  commands: (string * blob_digest list * Token.T list lazy) Inttab.table,
     1.8 -    (*command id -> name, inlined files, command span*)
     1.9 +  commands: (string * blob_digest list * int * Token.T list lazy) Inttab.table,
    1.10 +    (*command id -> name, inlined files, token index of files, command span*)
    1.11    execution: execution}  (*current execution process*)
    1.12  with
    1.13  
    1.14 @@ -385,7 +385,7 @@
    1.15                    else ();
    1.16                in tokens end) ());
    1.17        val commands' =
    1.18 -        Inttab.update_new (command_id, (name, command_blobs, span)) commands
    1.19 +        Inttab.update_new (command_id, (name, command_blobs, blobs_index, span)) commands
    1.20            handle Inttab.DUP dup => err_dup "command" dup;
    1.21        val _ =
    1.22          Position.setmp_thread_data (Position.id_only id)
    1.23 @@ -419,7 +419,7 @@
    1.24                SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
    1.25      val blobs' =
    1.26        (commands', Symtab.empty) |->
    1.27 -        Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
    1.28 +        Inttab.fold (fn (_, (_, blobs, _, _)) => blobs |>
    1.29            fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
    1.30  
    1.31    in (versions', blobs', commands', execution) end);
    1.32 @@ -585,13 +585,13 @@
    1.33  
    1.34        val command_visible = visible_command node command_id';
    1.35        val command_overlays = overlays node command_id';
    1.36 -      val (command_name, blob_digests, span0) = the_command state command_id';
    1.37 +      val (command_name, blob_digests, blobs_index, span0) = the_command state command_id';
    1.38        val blobs = map (resolve_blob state) blob_digests;
    1.39        val span = Lazy.force span0;
    1.40  
    1.41        val eval' =
    1.42          Command.eval keywords (master_directory node)
    1.43 -          (fn () => the_default illegal_init init span) blobs span eval;
    1.44 +          (fn () => the_default illegal_init init span) (blobs, blobs_index) span eval;
    1.45        val prints' =
    1.46          perhaps (Command.print command_visible command_overlays keywords command_name eval') [];
    1.47        val exec' = (eval', prints');