# HG changeset patch
# User wenzelm
# Date 1407577438 -7200
# Node ID 9c361f94b3232d79dd7b4bbee79f1b288fbfba0c
# Parent  ea94d2aa62be57011a754e2a9734342722fc8cee
tuned comments;

diff -r ea94d2aa62be -r 9c361f94b323 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Aug 09 11:25:46 2014 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Aug 09 11:43:58 2014 +0200
@@ -48,7 +48,7 @@
  {required: bool,  (*required node*)
   visible: Inttab.set,  (*visible commands*)
   visible_last: Document_ID.command option,  (*last visible command*)
-  overlays: (string * string list) list Inttab.table};  (*command id -> print function with args*)
+  overlays: (string * string list) list Inttab.table};  (*command id -> print functions with args*)
 
 structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);