src/Pure/PIDE/protocol.ML
changeset 46938 cda018294515
parent 46774 38f113b052b1
child 47343 b8aeab386414
--- a/src/Pure/PIDE/protocol.ML	Wed Mar 14 22:34:18 2012 +0100
+++ b/src/Pure/PIDE/protocol.ML	Thu Mar 15 00:10:45 2012 +0100
@@ -46,9 +46,16 @@
                  [fn ([], []) => Document.Clear,
                   fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
                   fn ([], a) =>
-                    Document.Header
-                      (Exn.Res
-                        (triple (pair string string) (list string) (list (pair string bool)) a)),
+                    let
+                      val ((((master, name), imports), keywords), uses) =
+                        pair (pair (pair (pair string string) (list string))
+                          (list (pair string (option (pair string (list string))))))
+                          (list (pair string bool)) a;
+                      val res =
+                        Exn.capture (fn () =>
+                          (master, Thy_Header.make name imports keywords
+                            (map (apfst Path.explode) uses))) ();
+                    in Document.Header res end,
                   fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
                   fn (a, []) => Document.Perspective (map int_atom a)]))
             end;