# HG changeset patch # User wenzelm # Date 1281480367 -7200 # Node ID 36187e8443dd98f3a4d82a5933c79e22c4b1a7cc # Parent 71bb3c273dd1f51a3faf891940290ce467dd3636 Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation; diff -r 71bb3c273dd1 -r 36187e8443dd src/Pure/Isar/isar_document.ML --- a/src/Pure/Isar/isar_document.ML Wed Aug 11 00:44:48 2010 +0200 +++ b/src/Pure/Isar/isar_document.ML Wed Aug 11 00:46:07 2010 +0200 @@ -143,10 +143,16 @@ in -fun define_command (id: Document.command_id) tr = - NAMED_CRITICAL "Isar" (fn () => - Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr)) - handle Symtab.DUP dup => err_dup "command" dup); +fun define_command (id: Document.command_id) text = + let + val tr = + Position.setmp_thread_data (Position.id_only id) (fn () => + Outer_Syntax.prepare_command (Position.id id) text) (); + in + NAMED_CRITICAL "Isar" (fn () => + Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr)) + handle Symtab.DUP dup => err_dup "command" dup) + end; fun the_command (id: Document.command_id) = (case Symtab.lookup (! global_commands) id of @@ -178,7 +184,7 @@ -(** main operations **) +(** document editing **) (* execution *) @@ -241,52 +247,50 @@ in fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits = - NAMED_CRITICAL "Isar" (fn () => - let - val old_document = the_document old_id; - val new_document = fold edit_nodes edits old_document; + Position.setmp_thread_data (Position.id_only new_id) (fn () => + NAMED_CRITICAL "Isar" (fn () => + let + val old_document = the_document old_id; + val new_document = fold edit_nodes edits old_document; - fun update_node name node = - (case first_entry (is_changed (the_node old_document name)) node of - NONE => ([], node) - | SOME (prev, id, _) => - let - val prev_state_id = the (#state (the_entry node (the prev))); - val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []); - val node' = fold set_entry_state updates node; - in (rev updates, node') end); + fun update_node name node = + (case first_entry (is_changed (the_node old_document name)) node of + NONE => ([], node) + | SOME (prev, id, _) => + let + val prev_state_id = the (#state (the_entry node (the prev))); + val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []); + val node' = fold set_entry_state updates node; + in (rev updates, node') end); - (* FIXME proper node deps *) - val (updatess, new_document') = - (Graph.keys new_document, new_document) - |-> fold_map (fn name => Graph.map_node_yield name (update_node name)); + (* FIXME proper node deps *) + val (updatess, new_document') = + (Graph.keys new_document, new_document) + |-> fold_map (fn name => Graph.map_node_yield name (update_node name)); - val _ = define_document new_id new_document'; - val _ = updates_status (flat updatess); - val _ = execute new_document'; - in () end); + val _ = define_document new_id new_document'; + val _ = updates_status (flat updatess); + val _ = execute new_document'; + in () end)) (); end; -(** concrete syntax **) +(** Isabelle process commands **) + +val _ = + Isabelle_Process.add_command "Isar_Document.define_command" + (fn [id, text] => define_command id text); val _ = - Outer_Syntax.internal_command "Isar.define_command" - (Parse.string -- Parse.string >> (fn (id, text) => - Toplevel.position (Position.id_only id) o - Toplevel.imperative (fn () => - define_command id (Outer_Syntax.prepare_command (Position.id id) text)))); - -val _ = - Outer_Syntax.internal_command "Isar.edit_document" - (Parse.string -- Parse.string -- - Parse_Value.list - (Parse.string -- Scan.option (Parse_Value.list (Parse.string -- Scan.option Parse.string))) - >> (fn ((old_id, new_id), edits) => - Toplevel.position (Position.id_only new_id) o - Toplevel.imperative (fn () => edit_document old_id new_id edits))); + Isabelle_Process.add_command "Isar_Document.edit_document" + (fn [old_id, new_id, edits] => + edit_document old_id new_id + (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string + (XML_Data.dest_option (XML_Data.dest_list + (XML_Data.dest_pair XML_Data.dest_string + (XML_Data.dest_option XML_Data.dest_string))))) (YXML.parse_body edits))); end; diff -r 71bb3c273dd1 -r 36187e8443dd src/Pure/Isar/isar_document.scala --- a/src/Pure/Isar/isar_document.scala Wed Aug 11 00:44:48 2010 +0200 +++ b/src/Pure/Isar/isar_document.scala Wed Aug 11 00:46:07 2010 +0200 @@ -37,10 +37,8 @@ /* commands */ - def define_command(id: Document.Command_ID, text: String) { - input("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " + - Isabelle_Syntax.encode_string(text)) - } + def define_command(id: Document.Command_ID, text: String): Unit = + input("Isar_Document.define_command", id, text) /* documents */ @@ -48,38 +46,14 @@ def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID, edits: List[Document.Edit[Document.Command_ID]]) { - def append_edit( - edit: (Option[Document.Command_ID], Option[Document.Command_ID]), result: StringBuilder) - { - Isabelle_Syntax.append_string(edit._1 getOrElse Document.NO_ID, result) - edit._2 match { - case None => - case Some(id2) => - result.append(" ") - Isabelle_Syntax.append_string(id2, result) - } - } + def make_id1(id1: Option[Document.Command_ID]): XML.Body = + XML_Data.make_string(id1 getOrElse Document.NO_ID) + val arg = + XML_Data.make_list( + XML_Data.make_pair(XML_Data.make_string)( + XML_Data.make_option(XML_Data.make_list( + XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_string))))))(edits) - def append_node_edit( - edit: (String, Option[List[(Option[Document.Command_ID], Option[Document.Command_ID])]]), - result: StringBuilder) - { - Isabelle_Syntax.append_string(edit._1, result) - edit._2 match { - case None => - case Some(eds) => - result.append(" ") - Isabelle_Syntax.append_list(append_edit, eds, result) - } - } - - val buf = new StringBuilder(40) - buf.append("Isar.edit_document ") - Isabelle_Syntax.append_string(old_id, buf) - buf.append(" ") - Isabelle_Syntax.append_string(new_id, buf) - buf.append(" ") - Isabelle_Syntax.append_list(append_node_edit, edits, buf) - input(buf.toString) + input("Isar_Document.edit_document", old_id, new_id, YXML.string_of_body(arg)) } } diff -r 71bb3c273dd1 -r 36187e8443dd src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Aug 11 00:44:48 2010 +0200 +++ b/src/Pure/ROOT.ML Wed Aug 11 00:46:07 2010 +0200 @@ -230,7 +230,7 @@ use "Isar/proof_node.ML"; use "Isar/toplevel.ML"; -(*theory syntax*) +(*theory documents*) use "Thy/present.ML"; use "Thy/term_style.ML"; use "Thy/thy_output.ML"; @@ -239,7 +239,6 @@ use "old_goals.ML"; use "Isar/outer_syntax.ML"; use "Thy/thy_info.ML"; -use "Isar/isar_document.ML"; (*theory and proof operations*) use "Isar/rule_insts.ML"; @@ -257,6 +256,7 @@ use "System/session.ML"; use "System/isar.ML"; use "System/isabelle_process.ML"; +use "Isar/isar_document.ML"; (* miscellaneous tools and packages for Pure Isabelle *)