src/Pure/PIDE/document.ML
changeset 52510 a4a102237ded
parent 52509 2193d2c7f586
child 52511 d5d2093ff224
--- a/src/Pure/PIDE/document.ML	Wed Jul 03 16:19:57 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Jul 03 16:58:35 2013 +0200
@@ -450,7 +450,7 @@
       val read =
         Position.setmp_thread_data (Position.id_only exec_id'_string)
           (fn () =>
-            Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span
+            Command.read span
             |> modify_init
             |> Toplevel.put_id exec_id'_string);
       val exec' =