# HG changeset patch
# User wenzelm
# Date 1393584414 -3600
# Node ID 985bd3a325ab7effef2f43f0d7c16936bad8cd32
# Parent  6a59b4bb7506c2054e215cc7da3246dc7c09ac86
tuned signature;

diff -r 6a59b4bb7506 -r 985bd3a325ab src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Feb 28 11:13:25 2014 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Feb 28 11:46:54 2014 +0100
@@ -6,17 +6,15 @@
 
 signature COMMAND =
 sig
-  type 'a blob = (string * 'a option) Exn.result
-  type blob_digest = string blob
-  type content = SHA1.digest * string list
+  type blob = (string * (SHA1.digest * string list) option) Exn.result
   val read_file: Path.T -> Position.T -> Path.T -> Token.file
-  val read: (unit -> theory) -> Path.T -> content blob list -> Token.T list -> Toplevel.transition
+  val read: (unit -> theory) -> Path.T -> blob list -> Token.T list -> Toplevel.transition
   type eval
   val eval_eq: eval * eval -> bool
   val eval_running: eval -> bool
   val eval_finished: eval -> bool
   val eval_result_state: eval -> Toplevel.state
-  val eval: (unit -> theory) -> Path.T -> content blob list -> Token.T list -> eval -> eval
+  val eval: (unit -> theory) -> Path.T -> blob list -> Token.T list -> eval -> eval
   type print
   val print: bool -> (string * string list) list -> string ->
     eval -> print list -> print list option
@@ -88,9 +86,8 @@
 
 (* read *)
 
-type 'a blob = (string * 'a option) Exn.result;  (*file node name, content*)
-type blob_digest = string blob;  (*raw digest*)
-type content = SHA1.digest * string list;  (*digest, lines*)
+type blob =
+  (string * (SHA1.digest * string list) option) Exn.result;  (*file node name, digest, lines*)
 
 fun read_file master_dir pos src_path =
   let
@@ -103,7 +100,7 @@
 
 local
 
-fun blob_file src_path file (digest, lines) =
+fun blob_file src_path lines digest file =
   let
     val file_pos =
       Position.file file (*sic!*) |>
@@ -119,9 +116,9 @@
         let
           fun make_file src_path (Exn.Res (_, NONE)) =
                 Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
-            | make_file src_path (Exn.Res (file, SOME content)) =
+            | make_file src_path (Exn.Res (file, SOME (digest, lines))) =
                (Position.report pos (Markup.path file);
-                Exn.Res (blob_file src_path file content))
+                Exn.Res (blob_file src_path lines digest file))
             | make_file _ (Exn.Exn e) = Exn.Exn e;
           val src_paths = Keyword.command_files cmd path;
         in
diff -r 6a59b4bb7506 -r 985bd3a325ab src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Feb 28 11:13:25 2014 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Feb 28 11:46:54 2014 +0100
@@ -18,7 +18,8 @@
   type state
   val init_state: state
   val define_blob: string -> string -> state -> state
-  val define_command: Document_ID.command -> string -> Command.blob_digest list -> string ->
+  type blob_digest = (string * string option) Exn.result
+  val define_command: Document_ID.command -> string -> blob_digest list -> string ->
     state -> state
   val remove_versions: Document_ID.version list -> state -> state
   val start_execution: state -> state
@@ -218,6 +219,8 @@
 
 (** main state -- document structure and execution process **)
 
+type blob_digest = (string * string option) Exn.result;  (* file name, raw digest*)
+
 type execution =
  {version_id: Document_ID.version,  (*static version id*)
   execution_id: Document_ID.execution,  (*dynamic execution id*)
@@ -234,8 +237,8 @@
 
 abstype state = State of
  {versions: version Inttab.table,  (*version id -> document content*)
-  blobs: (SHA1.digest * string list) Symtab.table,  (*digest -> digest, lines*)
-  commands: (string * Command.blob_digest list * Token.T list lazy) Inttab.table,
+  blobs: (SHA1.digest * string list) Symtab.table,  (*raw digest -> digest, lines*)
+  commands: (string * blob_digest list * Token.T list lazy) Inttab.table,
     (*command id -> name, inlined files, command span*)
   execution: execution}  (*current execution process*)
 with