src/Pure/PIDE/document.ML
changeset 57874 9c361f94b323
parent 57643 858bee39acde
child 57905 c0c5652e796e
     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