src/Pure/PIDE/document.ML
changeset 48918 6e5fd4585512
parent 48772 e46cd0d26481
child 48927 ef462b5558eb
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 24 11:32:12 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 24 12:35:39 2012 +0200
     1.3 @@ -442,15 +442,19 @@
     1.4          else (I, init);
     1.5        val exec_id' = new_id ();
     1.6        val exec_id'_string = print_id exec_id';
     1.7 -      val tr =
     1.8 +      val cmd =
     1.9          Position.setmp_thread_data (Position.id_only exec_id'_string)
    1.10            (fn () =>
    1.11 -            #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
    1.12 -            |> modify_init
    1.13 -            |> Toplevel.put_id exec_id'_string);
    1.14 +            let
    1.15 +              val tr =
    1.16 +                #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
    1.17 +                |> modify_init
    1.18 +                |> Toplevel.put_id exec_id'_string;
    1.19 +              val cmts = Outer_Syntax.span_cmts span;
    1.20 +            in (tr, cmts) end);
    1.21        val exec' =
    1.22          Command.memo (fn () =>
    1.23 -          Command.run_command (tr ()) (fst (Command.memo_result (snd (snd command_exec)))));
    1.24 +          Command.run_command (cmd ()) (fst (Command.memo_result (snd (snd command_exec)))));
    1.25        val command_exec' = (command_id', (exec_id', exec'));
    1.26      in SOME (command_exec' :: execs, command_exec', init') end;
    1.27