# HG changeset patch
# User wenzelm
# Date 1502107584 -7200
# Node ID d003b44674c1947d4059e03dc96f77b16d9440d4
# Parent  26735fab7a8f965c56d9d351618624a717332394
tuned spelling;

diff -r 26735fab7a8f -r d003b44674c1 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Aug 07 11:34:32 2017 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Aug 07 14:06:24 2017 +0200
@@ -58,7 +58,7 @@
  {header: node_header,  (*master directory, theory header, errors*)
   keywords: Keyword.keywords option,  (*outer syntax keywords*)
   perspective: perspective,  (*command perspective*)
-  entries: Command.exec option Entries.T,  (*command entries with excecutions*)
+  entries: Command.exec option Entries.T,  (*command entries with executions*)
   result: Command.eval option}  (*result of last execution*)
 and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
 with