# HG changeset patch # User wenzelm # Date 1393584494 -3600 # Node ID a1a8378bda422b2b2ccdf4564f59d095134aae40 # Parent 985bd3a325ab7effef2f43f0d7c16936bad8cd32 tuned comment; diff -r 985bd3a325ab -r a1a8378bda42 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Feb 28 11:46:54 2014 +0100 +++ b/src/Pure/PIDE/document.ML Fri Feb 28 11:48:14 2014 +0100 @@ -219,7 +219,7 @@ (** main state -- document structure and execution process **) -type blob_digest = (string * string option) Exn.result; (* file name, raw digest*) +type blob_digest = (string * string option) Exn.result; (* file node name, raw digest*) type execution = {version_id: Document_ID.version, (*static version id*)