src/Pure/PIDE/document.ML
changeset 55799 a1a8378bda42
parent 55798 985bd3a325ab
child 56208 06cc31dff138
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Feb 28 11:46:54 2014 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Feb 28 11:48:14 2014 +0100
     1.3 @@ -219,7 +219,7 @@
     1.4  
     1.5  (** main state -- document structure and execution process **)
     1.6  
     1.7 -type blob_digest = (string * string option) Exn.result;  (* file name, raw digest*)
     1.8 +type blob_digest = (string * string option) Exn.result;  (* file node name, raw digest*)
     1.9  
    1.10  type execution =
    1.11   {version_id: Document_ID.version,  (*static version id*)