src/Pure/PIDE/protocol.ML
changeset 48755 393a37003851
parent 48707 ba531af91148
child 48864 3ee314ae1e0a
     1.1 --- a/src/Pure/PIDE/protocol.ML	Fri Aug 10 13:33:07 2012 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Aug 10 15:14:45 2012 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4              let open XML.Decode in
     1.5                list (pair string
     1.6                  (variant
     1.7 -                 [fn ([], []) => Document.Clear,
     1.8 +                 [fn ([], []) => Document.Clear,  (* FIXME unused !? *)
     1.9                    fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
    1.10                    fn ([], a) =>
    1.11                      let