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