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