src/Pure/PIDE/command.ML
changeset 57905 c0c5652e796e
parent 57844 ae3eac418c5f
child 58853 f8715e7c1be6
--- 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