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' =