--- a/src/Pure/PIDE/isar_document.scala Thu Sep 01 23:08:42 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala Fri Sep 02 11:52:13 2011 +0200
@@ -148,8 +148,9 @@
{
/* commands */
- def define_command(id: Document.Command_ID, text: String): Unit =
- input("Isar_Document.define_command", Document.ID(id), text)
+ def define_command(command: Command): Unit =
+ input("Isar_Document.define_command",
+ Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
/* document versions */