src/Pure/PIDE/isar_document.ML
changeset 44384 8f6054a63f96
parent 44301 65f60d9ac4bf
child 44436 546adfa8a6fc
     1.1 --- a/src/Pure/PIDE/isar_document.ML	Mon Aug 22 21:09:26 2011 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.ML	Mon Aug 22 21:42:02 2011 +0200
     1.3 @@ -27,7 +27,8 @@
     1.4                    fn ([], a) =>
     1.5                      Document.Header
     1.6                        (Exn.Res (triple string (list string) (list (pair string bool)) a)),
     1.7 -                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
     1.8 +                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
     1.9 +                  fn (a, []) => Document.Perspective (map int_atom a)]))
    1.10              end;
    1.11  
    1.12        val running = Document.cancel_execution state;