tuned comments;
authorwenzelm
Sat, 09 Aug 2014 11:43:58 +0200
changeset 590909c361f94b323
parent 59089 ea94d2aa62be
child 59091 4ee24ee8055b
tuned comments;
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Aug 09 11:25:46 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Aug 09 11:43:58 2014 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4   {required: bool,  (*required node*)
     1.5    visible: Inttab.set,  (*visible commands*)
     1.6    visible_last: Document_ID.command option,  (*last visible command*)
     1.7 -  overlays: (string * string list) list Inttab.table};  (*command id -> print function with args*)
     1.8 +  overlays: (string * string list) list Inttab.table};  (*command id -> print functions with args*)
     1.9  
    1.10  structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
    1.11