src/Pure/PIDE/document.ML
changeset 55788 67699e08e969
parent 54562 301a721af68b
child 55798 985bd3a325ab
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Feb 27 17:24:46 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Feb 27 17:29:58 2014 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    type state
     1.5    val init_state: state
     1.6    val define_blob: string -> string -> state -> state
     1.7 -  val define_command: Document_ID.command -> string -> Command.blob list -> string ->
     1.8 +  val define_command: Document_ID.command -> string -> Command.blob_digest list -> string ->
     1.9      state -> state
    1.10    val remove_versions: Document_ID.version list -> state -> state
    1.11    val start_execution: state -> state
    1.12 @@ -234,8 +234,8 @@
    1.13  
    1.14  abstype state = State of
    1.15   {versions: version Inttab.table,  (*version id -> document content*)
    1.16 -  blobs: string Symtab.table,  (*digest -> text*)
    1.17 -  commands: (string * Command.blob list * Token.T list lazy) Inttab.table,
    1.18 +  blobs: (SHA1.digest * string list) Symtab.table,  (*digest -> digest, lines*)
    1.19 +  commands: (string * Command.blob_digest list * Token.T list lazy) Inttab.table,
    1.20      (*command id -> name, inlined files, command span*)
    1.21    execution: execution}  (*current execution process*)
    1.22  with
    1.23 @@ -275,13 +275,18 @@
    1.24  
    1.25  fun define_blob digest text =
    1.26    map_state (fn (versions, blobs, commands, execution) =>
    1.27 -    let val blobs' = Symtab.update (digest, text) blobs
    1.28 +    let
    1.29 +      val sha1_digest = SHA1.digest text;
    1.30 +      val _ =
    1.31 +        digest = SHA1.rep sha1_digest orelse
    1.32 +          error ("Ill-defined blob: bad SHA1 digest " ^ digest ^ " vs. " ^ SHA1.rep sha1_digest);
    1.33 +      val blobs' = Symtab.update (digest, (sha1_digest, split_lines text)) blobs;
    1.34      in (versions, blobs', commands, execution) end);
    1.35  
    1.36  fun the_blob (State {blobs, ...}) digest =
    1.37    (case Symtab.lookup blobs digest of
    1.38      NONE => error ("Undefined blob: " ^ digest)
    1.39 -  | SOME text => text);
    1.40 +  | SOME content => content);
    1.41  
    1.42  
    1.43  (* commands *)
    1.44 @@ -496,8 +501,8 @@
    1.45  
    1.46        val command_visible = visible_command node command_id';
    1.47        val command_overlays = overlays node command_id';
    1.48 -      val (command_name, blobs0, span0) = the_command state command_id';
    1.49 -      val blobs = (map o Exn.map_result o apsnd o Option.map) (the_blob state) blobs0;
    1.50 +      val (command_name, blob_digests, span0) = the_command state command_id';
    1.51 +      val blobs = (map o Exn.map_result o apsnd o Option.map) (the_blob state) blob_digests;
    1.52        val span = Lazy.force span0;
    1.53  
    1.54        val eval' =