src/Pure/PIDE/document.ML
changeset 47395 e6261a493f04
parent 47389 e8552cba702d
child 47404 e6e5750f1311
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Apr 07 18:08:29 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Apr 07 19:28:44 2012 +0200
     1.3 @@ -276,7 +276,15 @@
     1.4  fun define_command (id: command_id) name text =
     1.5    map_state (fn (versions, commands, execution) =>
     1.6      let
     1.7 -      val span = Lazy.lazy (fn () => Command.parse_command (print_id id) text);
     1.8 +      val id_string = print_id id;
     1.9 +      val span = Lazy.lazy (fn () =>
    1.10 +        Position.setmp_thread_data (Position.id_only id_string)
    1.11 +          (fn () =>
    1.12 +            Thy_Syntax.parse_tokens
    1.13 +              (#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ());
    1.14 +      val _ =
    1.15 +        Position.setmp_thread_data (Position.id_only id_string)
    1.16 +          (fn () => Output.status (Markup.markup_only Isabelle_Markup.accepted)) ();
    1.17        val commands' =
    1.18          Inttab.update_new (id, (name, span)) commands
    1.19            handle Inttab.DUP dup => err_dup "command" dup;