# HG changeset patch # User wenzelm # Date 1282215108 -7200 # Node ID 3d16bebee1d34ec64ae48930b8082b8f6736709b # Parent 7b6ee937b75fcaab596cabfecff65b99395e7ce7 moved Isar_Document to Pure/PIDE; diff -r 7b6ee937b75f -r 3d16bebee1d3 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Thu Aug 19 12:41:40 2010 +0200 +++ b/src/Pure/IsaMakefile Thu Aug 19 12:51:48 2010 +0200 @@ -157,6 +157,7 @@ ML/ml_syntax.ML \ ML/ml_thms.ML \ PIDE/document.ML \ + PIDE/isar_document.ML \ Proof/extraction.ML \ Proof/proof_rewrite_rules.ML \ Proof/proof_syntax.ML \ @@ -188,7 +189,6 @@ Syntax/type_ext.ML \ System/isabelle_process.ML \ System/isar.ML \ - System/isar_document.ML \ System/session.ML \ Thy/html.ML \ Thy/latex.ML \ diff -r 7b6ee937b75f -r 3d16bebee1d3 src/Pure/PIDE/isar_document.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/isar_document.ML Thu Aug 19 12:51:48 2010 +0200 @@ -0,0 +1,42 @@ +(* Title: Pure/PIDE/isar_document.ML + Author: Makarius + +Protocol commands for interactive Isar documents. +*) + +structure Isar_Document: sig end = +struct + +val global_state = Synchronized.var "Isar_Document" Document.init_state; +val change_state = Synchronized.change global_state; + +val _ = + Isabelle_Process.add_command "Isar_Document.define_command" + (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text)); + +val _ = + Isabelle_Process.add_command "Isar_Document.edit_version" + (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state => + let + val old_id = Document.parse_id old_id_string; + val new_id = Document.parse_id new_id_string; + val edits = + 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_option XML_Data.dest_int) + (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml); + + val (updates, state') = Document.edit old_id new_id edits state; + val _ = + implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates) + |> Markup.markup (Markup.assign new_id) + |> Output.status; + val state'' = Document.execute new_id state'; + in state'' end)); + +end; + diff -r 7b6ee937b75f -r 3d16bebee1d3 src/Pure/PIDE/isar_document.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/isar_document.scala Thu Aug 19 12:51:48 2010 +0200 @@ -0,0 +1,65 @@ +/* Title: Pure/PIDE/isar_document.scala + Author: Makarius + +Protocol commands for interactive Isar documents. +*/ + +package isabelle + + +object Isar_Document +{ + /* protocol messages */ + + object Assign { + def unapply(msg: XML.Tree) + : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] = + msg match { + case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) => + val id_edits = edits.map(Edit.unapply) + if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get))) + else None + case _ => None + } + } + + object Edit { + def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] = + msg match { + case XML.Elem( + Markup(Markup.EDIT, + List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j)) + case _ => None + } + } +} + + +trait Isar_Document extends Isabelle_Process +{ + import Isar_Document._ + + + /* commands */ + + def define_command(id: Document.Command_ID, text: String): Unit = + input("Isar_Document.define_command", Document.ID(id), text) + + + /* document versions */ + + def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID, + edits: List[Document.Edit[Document.Command_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( + XML_Data.make_option(XML_Data.make_long))( + XML_Data.make_option(XML_Data.make_long))))))(edits) + + input("Isar_Document.edit_version", + Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg)) + } +} diff -r 7b6ee937b75f -r 3d16bebee1d3 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Aug 19 12:41:40 2010 +0200 +++ b/src/Pure/ROOT.ML Thu Aug 19 12:51:48 2010 +0200 @@ -257,7 +257,7 @@ use "System/session.ML"; use "System/isabelle_process.ML"; -use "System/isar_document.ML"; +use "PIDE/isar_document.ML"; use "System/isar.ML"; diff -r 7b6ee937b75f -r 3d16bebee1d3 src/Pure/System/isar_document.ML --- a/src/Pure/System/isar_document.ML Thu Aug 19 12:41:40 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,42 +0,0 @@ -(* Title: Pure/System/isar_document.ML - Author: Makarius - -Protocol commands for interactive Isar documents. -*) - -structure Isar_Document: sig end = -struct - -val global_state = Synchronized.var "Isar_Document" Document.init_state; -val change_state = Synchronized.change global_state; - -val _ = - Isabelle_Process.add_command "Isar_Document.define_command" - (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text)); - -val _ = - Isabelle_Process.add_command "Isar_Document.edit_version" - (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state => - let - val old_id = Document.parse_id old_id_string; - val new_id = Document.parse_id new_id_string; - val edits = - 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_option XML_Data.dest_int) - (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml); - - val (updates, state') = Document.edit old_id new_id edits state; - val _ = - implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates) - |> Markup.markup (Markup.assign new_id) - |> Output.status; - val state'' = Document.execute new_id state'; - in state'' end)); - -end; - diff -r 7b6ee937b75f -r 3d16bebee1d3 src/Pure/System/isar_document.scala --- a/src/Pure/System/isar_document.scala Thu Aug 19 12:41:40 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,65 +0,0 @@ -/* Title: Pure/System/isar_document.scala - Author: Makarius - -Protocol commands for interactive Isar documents. -*/ - -package isabelle - - -object Isar_Document -{ - /* protocol messages */ - - object Assign { - def unapply(msg: XML.Tree) - : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] = - msg match { - case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) => - val id_edits = edits.map(Edit.unapply) - if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get))) - else None - case _ => None - } - } - - object Edit { - def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] = - msg match { - case XML.Elem( - Markup(Markup.EDIT, - List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j)) - case _ => None - } - } -} - - -trait Isar_Document extends Isabelle_Process -{ - import Isar_Document._ - - - /* commands */ - - def define_command(id: Document.Command_ID, text: String): Unit = - input("Isar_Document.define_command", Document.ID(id), text) - - - /* document versions */ - - def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID, - edits: List[Document.Edit[Document.Command_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( - XML_Data.make_option(XML_Data.make_long))( - XML_Data.make_option(XML_Data.make_long))))))(edits) - - input("Isar_Document.edit_version", - Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg)) - } -} diff -r 7b6ee937b75f -r 3d16bebee1d3 src/Pure/build-jars --- a/src/Pure/build-jars Thu Aug 19 12:41:40 2010 +0200 +++ b/src/Pure/build-jars Thu Aug 19 12:51:48 2010 +0200 @@ -41,6 +41,7 @@ Isar/token.scala PIDE/command.scala PIDE/document.scala + PIDE/isar_document.scala PIDE/markup_tree.scala PIDE/text.scala System/cygwin.scala @@ -50,7 +51,6 @@ System/isabelle_process.scala System/isabelle_syntax.scala System/isabelle_system.scala - System/isar_document.scala System/platform.scala System/session.scala System/session_manager.scala