src/Pure/PIDE/document.ML
changeset 48755 393a37003851
parent 48735 35c47932584c
child 48772 e46cd0d26481
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 10 13:33:07 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 10 15:14:45 2012 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val print_id: id -> string
     1.5    type node_header = string * Thy_Header.header * string list
     1.6    datatype node_edit =
     1.7 -    Clear |
     1.8 +    Clear |    (* FIXME unused !? *)
     1.9      Edits of (command_id option * command_id option) list |
    1.10      Deps of node_header |
    1.11      Perspective of command_id list