36 open XML.Decode; |
36 open XML.Decode; |
37 val (blobs_digests, blobs_index) = |
37 val (blobs_digests, blobs_index) = |
38 blobs_xml |> |
38 blobs_xml |> |
39 let |
39 let |
40 val message = YXML.string_of_body o Protocol_Message.command_positions id; |
40 val message = YXML.string_of_body o Protocol_Message.command_positions id; |
|
41 val blob = |
|
42 triple string string (option string) |
|
43 #> (fn (a, b, c) => {file_node = a, src_path = Path.explode b, digest = c}); |
41 in |
44 in |
42 pair |
45 pair |
43 (list (variant |
46 (list (variant |
44 [fn ([], a) => Exn.Res (pair string (option string) a), |
47 [fn ([], a) => Exn.Res (blob a), |
45 fn ([], a) => Exn.Exn (ERROR (message a))])) |
48 fn ([], a) => Exn.Exn (ERROR (message a))])) |
46 int |
49 int |
47 end; |
50 end; |
48 val toks = list (pair int int) toks_xml; |
51 val toks = list (pair int int) toks_xml; |
49 in |
52 in |
107 [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), |
110 [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), |
108 fn ([], a) => |
111 fn ([], a) => |
109 let |
112 let |
110 val (master, (name, (imports, (keywords, errors)))) = |
113 val (master, (name, (imports, (keywords, errors)))) = |
111 pair string (pair string (pair (list string) |
114 pair string (pair string (pair (list string) |
112 (pair (list (pair string |
115 (pair (list (pair string (pair string (list string)))) |
113 (pair (pair string (list string)) (list string)))) |
|
114 (list YXML.string_of_body)))) a; |
116 (list YXML.string_of_body)))) a; |
115 val imports' = map (rpair Position.none) imports; |
117 val imports' = map (rpair Position.none) imports; |
116 val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords; |
118 val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords; |
117 val header = Thy_Header.make (name, Position.none) imports' keywords'; |
119 val header = Thy_Header.make (name, Position.none) imports' keywords'; |
118 in Document.Deps {master = master, header = header, errors = errors} end, |
120 in Document.Deps {master = master, header = header, errors = errors} end, |