40 val (master, (name, (imports, (keywords, (uses, errors))))) = |
40 val (master, (name, (imports, (keywords, (uses, errors))))) = |
41 pair string (pair string (pair (list string) |
41 pair string (pair string (pair (list string) |
42 (pair (list (pair string |
42 (pair (list (pair string |
43 (option (pair (pair string (list string)) (list string))))) |
43 (option (pair (pair string (list string)) (list string))))) |
44 (pair (list (pair string bool)) (list string))))) a; |
44 (pair (list (pair string bool)) (list string))))) a; |
|
45 val imports' = map (rpair Position.none) imports; |
45 val (uses', errors') = |
46 val (uses', errors') = |
46 (map (apfst Path.explode) uses, errors) |
47 (map (apfst Path.explode) uses, errors) |
47 handle ERROR msg => ([], errors @ [msg]); |
48 handle ERROR msg => ([], errors @ [msg]); |
48 val header = Thy_Header.make name imports keywords uses'; |
49 val header = Thy_Header.make (name, Position.none) imports' keywords uses'; |
49 in Document.Deps (master, header, errors') end, |
50 in Document.Deps (master, header, errors') end, |
50 fn (a, []) => Document.Perspective (map int_atom a)])) |
51 fn (a, []) => Document.Perspective (map int_atom a)])) |
51 end; |
52 end; |
52 |
53 |
53 val (assignment, state') = Document.update old_id new_id edits state; |
54 val (assignment, state') = Document.update old_id new_id edits state; |