1.1 --- a/src/Pure/PIDE/protocol.ML	Wed Mar 14 22:34:18 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Mar 15 00:10:45 2012 +0100
     1.3 @@ -46,9 +46,16 @@
     1.4                   [fn ([], []) => Document.Clear,
     1.5                    fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
     1.6                    fn ([], a) =>
     1.7 -                    Document.Header
     1.8 -                      (Exn.Res
     1.9 -                        (triple (pair string string) (list string) (list (pair string bool)) a)),
    1.10 +                    let
    1.11 +                      val ((((master, name), imports), keywords), uses) =
    1.12 +                        pair (pair (pair (pair string string) (list string))
    1.13 +                          (list (pair string (option (pair string (list string))))))
    1.14 +                          (list (pair string bool)) a;
    1.15 +                      val res =
    1.16 +                        Exn.capture (fn () =>
    1.17 +                          (master, Thy_Header.make name imports keywords
    1.18 +                            (map (apfst Path.explode) uses))) ();
    1.19 +                    in Document.Header res end,
    1.20                    fn ([a], []) => Document.Header (Exn.Exn (ERROR a)),
    1.21                    fn (a, []) => Document.Perspective (map int_atom a)]))
    1.22              end;