tuned signature;
authorwenzelm
Fri Feb 28 11:46:54 2014 +0100 (2014-02-28)
changeset 55798985bd3a325ab
parent 55797 6a59b4bb7506
child 55799 a1a8378bda42
tuned signature;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Fri Feb 28 11:13:25 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Fri Feb 28 11:46:54 2014 +0100
     1.3 @@ -6,17 +6,15 @@
     1.4  
     1.5  signature COMMAND =
     1.6  sig
     1.7 -  type 'a blob = (string * 'a option) Exn.result
     1.8 -  type blob_digest = string blob
     1.9 -  type content = SHA1.digest * string list
    1.10 +  type blob = (string * (SHA1.digest * string list) option) Exn.result
    1.11    val read_file: Path.T -> Position.T -> Path.T -> Token.file
    1.12 -  val read: (unit -> theory) -> Path.T -> content blob list -> Token.T list -> Toplevel.transition
    1.13 +  val read: (unit -> theory) -> Path.T -> blob list -> Token.T list -> Toplevel.transition
    1.14    type eval
    1.15    val eval_eq: eval * eval -> bool
    1.16    val eval_running: eval -> bool
    1.17    val eval_finished: eval -> bool
    1.18    val eval_result_state: eval -> Toplevel.state
    1.19 -  val eval: (unit -> theory) -> Path.T -> content blob list -> Token.T list -> eval -> eval
    1.20 +  val eval: (unit -> theory) -> Path.T -> blob list -> Token.T list -> eval -> eval
    1.21    type print
    1.22    val print: bool -> (string * string list) list -> string ->
    1.23      eval -> print list -> print list option
    1.24 @@ -88,9 +86,8 @@
    1.25  
    1.26  (* read *)
    1.27  
    1.28 -type 'a blob = (string * 'a option) Exn.result;  (*file node name, content*)
    1.29 -type blob_digest = string blob;  (*raw digest*)
    1.30 -type content = SHA1.digest * string list;  (*digest, lines*)
    1.31 +type blob =
    1.32 +  (string * (SHA1.digest * string list) option) Exn.result;  (*file node name, digest, lines*)
    1.33  
    1.34  fun read_file master_dir pos src_path =
    1.35    let
    1.36 @@ -103,7 +100,7 @@
    1.37  
    1.38  local
    1.39  
    1.40 -fun blob_file src_path file (digest, lines) =
    1.41 +fun blob_file src_path lines digest file =
    1.42    let
    1.43      val file_pos =
    1.44        Position.file file (*sic!*) |>
    1.45 @@ -119,9 +116,9 @@
    1.46          let
    1.47            fun make_file src_path (Exn.Res (_, NONE)) =
    1.48                  Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
    1.49 -            | make_file src_path (Exn.Res (file, SOME content)) =
    1.50 +            | make_file src_path (Exn.Res (file, SOME (digest, lines))) =
    1.51                 (Position.report pos (Markup.path file);
    1.52 -                Exn.Res (blob_file src_path file content))
    1.53 +                Exn.Res (blob_file src_path lines digest file))
    1.54              | make_file _ (Exn.Exn e) = Exn.Exn e;
    1.55            val src_paths = Keyword.command_files cmd path;
    1.56          in
     2.1 --- a/src/Pure/PIDE/document.ML	Fri Feb 28 11:13:25 2014 +0100
     2.2 +++ b/src/Pure/PIDE/document.ML	Fri Feb 28 11:46:54 2014 +0100
     2.3 @@ -18,7 +18,8 @@
     2.4    type state
     2.5    val init_state: state
     2.6    val define_blob: string -> string -> state -> state
     2.7 -  val define_command: Document_ID.command -> string -> Command.blob_digest list -> string ->
     2.8 +  type blob_digest = (string * string option) Exn.result
     2.9 +  val define_command: Document_ID.command -> string -> blob_digest list -> string ->
    2.10      state -> state
    2.11    val remove_versions: Document_ID.version list -> state -> state
    2.12    val start_execution: state -> state
    2.13 @@ -218,6 +219,8 @@
    2.14  
    2.15  (** main state -- document structure and execution process **)
    2.16  
    2.17 +type blob_digest = (string * string option) Exn.result;  (* file name, raw digest*)
    2.18 +
    2.19  type execution =
    2.20   {version_id: Document_ID.version,  (*static version id*)
    2.21    execution_id: Document_ID.execution,  (*dynamic execution id*)
    2.22 @@ -234,8 +237,8 @@
    2.23  
    2.24  abstype state = State of
    2.25   {versions: version Inttab.table,  (*version id -> document content*)
    2.26 -  blobs: (SHA1.digest * string list) Symtab.table,  (*digest -> digest, lines*)
    2.27 -  commands: (string * Command.blob_digest list * Token.T list lazy) Inttab.table,
    2.28 +  blobs: (SHA1.digest * string list) Symtab.table,  (*raw digest -> digest, lines*)
    2.29 +  commands: (string * blob_digest list * Token.T list lazy) Inttab.table,
    2.30      (*command id -> name, inlined files, command span*)
    2.31    execution: execution}  (*current execution process*)
    2.32  with