tuned comments;
authorwenzelm
Sat, 09 Aug 2014 11:43:58 +0200
changeset 57874 9c361f94b323
parent 57873 ea94d2aa62be
child 57875 4ee24ee8055b
tuned comments;
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);