--- a/src/Pure/PIDE/document.ML Sat Apr 07 18:08:29 2012 +0200
+++ b/src/Pure/PIDE/document.ML Sat Apr 07 19:28:44 2012 +0200
@@ -276,7 +276,15 @@
fun define_command (id: command_id) name text =
map_state (fn (versions, commands, execution) =>
let
- val span = Lazy.lazy (fn () => Command.parse_command (print_id id) text);
+ val id_string = print_id id;
+ val span = Lazy.lazy (fn () =>
+ Position.setmp_thread_data (Position.id_only id_string)
+ (fn () =>
+ Thy_Syntax.parse_tokens
+ (#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ());
+ val _ =
+ Position.setmp_thread_data (Position.id_only id_string)
+ (fn () => Output.status (Markup.markup_only Isabelle_Markup.accepted)) ();
val commands' =
Inttab.update_new (id, (name, span)) commands
handle Inttab.DUP dup => err_dup "command" dup;