diff -r 922273b7bf8a -r c0c5652e796e src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Mon Aug 11 22:59:38 2014 +0200 +++ b/src/Pure/PIDE/command.ML Tue Aug 12 00:08:32 2014 +0200 @@ -121,9 +121,9 @@ in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end fun resolve_files master_dir blobs toks = - (case Thy_Syntax.parse_spans toks of + (case Outer_Syntax.parse_spans toks of [span] => span - |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) => + |> Command_Span.resolve_files (fn cmd => fn (path, pos) => let fun make_file src_path (Exn.Res (file_node, NONE)) = Exn.interruptible_capture (fn () => @@ -140,7 +140,7 @@ map2 make_file src_paths blobs else error ("Misalignment of inlined files" ^ Position.here pos) end) - |> Thy_Syntax.span_content + |> Command_Span.content | _ => toks); in