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*)