src/Pure/PIDE/document.ML
changeset 46910 3e068ef04b42
parent 46876 8f3bb485f628
child 46938 cda018294515
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Mar 13 20:04:24 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Mar 13 21:17:37 2012 +0100
     1.3 @@ -273,9 +273,13 @@
     1.4  
     1.5  (* commands *)
     1.6  
     1.7 -fun tokenize_command id text =
     1.8 +fun parse_command id text =
     1.9    Position.setmp_thread_data (Position.id_only id)
    1.10 -    (fn () => Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text) ();
    1.11 +    (fn () =>
    1.12 +      let
    1.13 +        val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text;
    1.14 +        val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed);
    1.15 +      in toks end) ();
    1.16  
    1.17  fun define_command (id: command_id) name text =
    1.18    map_state (fn (versions, commands, execution) =>
    1.19 @@ -284,7 +288,7 @@
    1.20          (singleton o Future.forks)
    1.21            {name = "Document.define_command", group = SOME (Future.new_group NONE),
    1.22              deps = [], pri = ~1, interrupts = false}
    1.23 -          (fn () => tokenize_command (print_id id) text);
    1.24 +          (fn () => parse_command (print_id id) text);
    1.25        val commands' =
    1.26          Inttab.update_new (id, (name, future)) commands
    1.27            handle Inttab.DUP dup => err_dup "command" dup;