src/Pure/PIDE/document.ML
changeset 55798 985bd3a325ab
parent 55788 67699e08e969
child 55799 a1a8378bda42
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Feb 28 11:13:25 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Feb 28 11:46:54 2014 +0100
     1.3 @@ -18,7 +18,8 @@
     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_digest list -> string ->
     1.8 +  type blob_digest = (string * string option) Exn.result
     1.9 +  val define_command: Document_ID.command -> string -> blob_digest 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 @@ -218,6 +219,8 @@
    1.14  
    1.15  (** main state -- document structure and execution process **)
    1.16  
    1.17 +type blob_digest = (string * string option) Exn.result;  (* file name, raw digest*)
    1.18 +
    1.19  type execution =
    1.20   {version_id: Document_ID.version,  (*static version id*)
    1.21    execution_id: Document_ID.execution,  (*dynamic execution id*)
    1.22 @@ -234,8 +237,8 @@
    1.23  
    1.24  abstype state = State of
    1.25   {versions: version Inttab.table,  (*version id -> document content*)
    1.26 -  blobs: (SHA1.digest * string list) Symtab.table,  (*digest -> digest, lines*)
    1.27 -  commands: (string * Command.blob_digest list * Token.T list lazy) Inttab.table,
    1.28 +  blobs: (SHA1.digest * string list) Symtab.table,  (*raw digest -> digest, lines*)
    1.29 +  commands: (string * blob_digest list * Token.T list lazy) Inttab.table,
    1.30      (*command id -> name, inlined files, command span*)
    1.31    execution: execution}  (*current execution process*)
    1.32  with