moved Isar_Document to Pure/PIDE;
authorwenzelm
Thu Aug 19 12:51:48 2010 +0200 (2010-08-19 ago)
changeset 384833d16bebee1d3
parent 38482 7b6ee937b75f
child 38484 9c1fde4e2487
moved Isar_Document to Pure/PIDE;
src/Pure/IsaMakefile
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
src/Pure/ROOT.ML
src/Pure/System/isar_document.ML
src/Pure/System/isar_document.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/IsaMakefile	Thu Aug 19 12:41:40 2010 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Thu Aug 19 12:51:48 2010 +0200
     1.3 @@ -157,6 +157,7 @@
     1.4    ML/ml_syntax.ML					\
     1.5    ML/ml_thms.ML						\
     1.6    PIDE/document.ML					\
     1.7 +  PIDE/isar_document.ML					\
     1.8    Proof/extraction.ML					\
     1.9    Proof/proof_rewrite_rules.ML				\
    1.10    Proof/proof_syntax.ML					\
    1.11 @@ -188,7 +189,6 @@
    1.12    Syntax/type_ext.ML					\
    1.13    System/isabelle_process.ML				\
    1.14    System/isar.ML					\
    1.15 -  System/isar_document.ML				\
    1.16    System/session.ML					\
    1.17    Thy/html.ML						\
    1.18    Thy/latex.ML						\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/PIDE/isar_document.ML	Thu Aug 19 12:51:48 2010 +0200
     2.3 @@ -0,0 +1,42 @@
     2.4 +(*  Title:      Pure/PIDE/isar_document.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Protocol commands for interactive Isar documents.
     2.8 +*)
     2.9 +
    2.10 +structure Isar_Document: sig end =
    2.11 +struct
    2.12 +
    2.13 +val global_state = Synchronized.var "Isar_Document" Document.init_state;
    2.14 +val change_state = Synchronized.change global_state;
    2.15 +
    2.16 +val _ =
    2.17 +  Isabelle_Process.add_command "Isar_Document.define_command"
    2.18 +    (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
    2.19 +
    2.20 +val _ =
    2.21 +  Isabelle_Process.add_command "Isar_Document.edit_version"
    2.22 +    (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
    2.23 +      let
    2.24 +        val old_id = Document.parse_id old_id_string;
    2.25 +        val new_id = Document.parse_id new_id_string;
    2.26 +        val edits =
    2.27 +          XML_Data.dest_list
    2.28 +            (XML_Data.dest_pair
    2.29 +              XML_Data.dest_string
    2.30 +              (XML_Data.dest_option
    2.31 +                (XML_Data.dest_list
    2.32 +                  (XML_Data.dest_pair
    2.33 +                    (XML_Data.dest_option XML_Data.dest_int)
    2.34 +                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
    2.35 +
    2.36 +      val (updates, state') = Document.edit old_id new_id edits state;
    2.37 +      val _ =
    2.38 +        implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
    2.39 +        |> Markup.markup (Markup.assign new_id)
    2.40 +        |> Output.status;
    2.41 +      val state'' = Document.execute new_id state';
    2.42 +    in state'' end));
    2.43 +
    2.44 +end;
    2.45 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/PIDE/isar_document.scala	Thu Aug 19 12:51:48 2010 +0200
     3.3 @@ -0,0 +1,65 @@
     3.4 +/*  Title:      Pure/PIDE/isar_document.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Protocol commands for interactive Isar documents.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +object Isar_Document
    3.14 +{
    3.15 +  /* protocol messages */
    3.16 +
    3.17 +  object Assign {
    3.18 +    def unapply(msg: XML.Tree)
    3.19 +        : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
    3.20 +      msg match {
    3.21 +        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
    3.22 +          val id_edits = edits.map(Edit.unapply)
    3.23 +          if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
    3.24 +          else None
    3.25 +        case _ => None
    3.26 +      }
    3.27 +  }
    3.28 +
    3.29 +  object Edit {
    3.30 +    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
    3.31 +      msg match {
    3.32 +        case XML.Elem(
    3.33 +          Markup(Markup.EDIT,
    3.34 +            List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
    3.35 +        case _ => None
    3.36 +      }
    3.37 +  }
    3.38 +}
    3.39 +
    3.40 +
    3.41 +trait Isar_Document extends Isabelle_Process
    3.42 +{
    3.43 +  import Isar_Document._
    3.44 +
    3.45 +
    3.46 +  /* commands */
    3.47 +
    3.48 +  def define_command(id: Document.Command_ID, text: String): Unit =
    3.49 +    input("Isar_Document.define_command", Document.ID(id), text)
    3.50 +
    3.51 +
    3.52 +  /* document versions */
    3.53 +
    3.54 +  def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
    3.55 +      edits: List[Document.Edit[Document.Command_ID]])
    3.56 +  {
    3.57 +    val arg =
    3.58 +      XML_Data.make_list(
    3.59 +        XML_Data.make_pair(XML_Data.make_string)(
    3.60 +          XML_Data.make_option(XML_Data.make_list(
    3.61 +              XML_Data.make_pair(
    3.62 +                XML_Data.make_option(XML_Data.make_long))(
    3.63 +                XML_Data.make_option(XML_Data.make_long))))))(edits)
    3.64 +
    3.65 +    input("Isar_Document.edit_version",
    3.66 +      Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
    3.67 +  }
    3.68 +}
     4.1 --- a/src/Pure/ROOT.ML	Thu Aug 19 12:41:40 2010 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Thu Aug 19 12:51:48 2010 +0200
     4.3 @@ -257,7 +257,7 @@
     4.4  
     4.5  use "System/session.ML";
     4.6  use "System/isabelle_process.ML";
     4.7 -use "System/isar_document.ML";
     4.8 +use "PIDE/isar_document.ML";
     4.9  use "System/isar.ML";
    4.10  
    4.11  
     5.1 --- a/src/Pure/System/isar_document.ML	Thu Aug 19 12:41:40 2010 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,42 +0,0 @@
     5.4 -(*  Title:      Pure/System/isar_document.ML
     5.5 -    Author:     Makarius
     5.6 -
     5.7 -Protocol commands for interactive Isar documents.
     5.8 -*)
     5.9 -
    5.10 -structure Isar_Document: sig end =
    5.11 -struct
    5.12 -
    5.13 -val global_state = Synchronized.var "Isar_Document" Document.init_state;
    5.14 -val change_state = Synchronized.change global_state;
    5.15 -
    5.16 -val _ =
    5.17 -  Isabelle_Process.add_command "Isar_Document.define_command"
    5.18 -    (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
    5.19 -
    5.20 -val _ =
    5.21 -  Isabelle_Process.add_command "Isar_Document.edit_version"
    5.22 -    (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
    5.23 -      let
    5.24 -        val old_id = Document.parse_id old_id_string;
    5.25 -        val new_id = Document.parse_id new_id_string;
    5.26 -        val edits =
    5.27 -          XML_Data.dest_list
    5.28 -            (XML_Data.dest_pair
    5.29 -              XML_Data.dest_string
    5.30 -              (XML_Data.dest_option
    5.31 -                (XML_Data.dest_list
    5.32 -                  (XML_Data.dest_pair
    5.33 -                    (XML_Data.dest_option XML_Data.dest_int)
    5.34 -                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
    5.35 -
    5.36 -      val (updates, state') = Document.edit old_id new_id edits state;
    5.37 -      val _ =
    5.38 -        implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
    5.39 -        |> Markup.markup (Markup.assign new_id)
    5.40 -        |> Output.status;
    5.41 -      val state'' = Document.execute new_id state';
    5.42 -    in state'' end));
    5.43 -
    5.44 -end;
    5.45 -
     6.1 --- a/src/Pure/System/isar_document.scala	Thu Aug 19 12:41:40 2010 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,65 +0,0 @@
     6.4 -/*  Title:      Pure/System/isar_document.scala
     6.5 -    Author:     Makarius
     6.6 -
     6.7 -Protocol commands for interactive Isar documents.
     6.8 -*/
     6.9 -
    6.10 -package isabelle
    6.11 -
    6.12 -
    6.13 -object Isar_Document
    6.14 -{
    6.15 -  /* protocol messages */
    6.16 -
    6.17 -  object Assign {
    6.18 -    def unapply(msg: XML.Tree)
    6.19 -        : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
    6.20 -      msg match {
    6.21 -        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
    6.22 -          val id_edits = edits.map(Edit.unapply)
    6.23 -          if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
    6.24 -          else None
    6.25 -        case _ => None
    6.26 -      }
    6.27 -  }
    6.28 -
    6.29 -  object Edit {
    6.30 -    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
    6.31 -      msg match {
    6.32 -        case XML.Elem(
    6.33 -          Markup(Markup.EDIT,
    6.34 -            List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
    6.35 -        case _ => None
    6.36 -      }
    6.37 -  }
    6.38 -}
    6.39 -
    6.40 -
    6.41 -trait Isar_Document extends Isabelle_Process
    6.42 -{
    6.43 -  import Isar_Document._
    6.44 -
    6.45 -
    6.46 -  /* commands */
    6.47 -
    6.48 -  def define_command(id: Document.Command_ID, text: String): Unit =
    6.49 -    input("Isar_Document.define_command", Document.ID(id), text)
    6.50 -
    6.51 -
    6.52 -  /* document versions */
    6.53 -
    6.54 -  def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
    6.55 -      edits: List[Document.Edit[Document.Command_ID]])
    6.56 -  {
    6.57 -    val arg =
    6.58 -      XML_Data.make_list(
    6.59 -        XML_Data.make_pair(XML_Data.make_string)(
    6.60 -          XML_Data.make_option(XML_Data.make_list(
    6.61 -              XML_Data.make_pair(
    6.62 -                XML_Data.make_option(XML_Data.make_long))(
    6.63 -                XML_Data.make_option(XML_Data.make_long))))))(edits)
    6.64 -
    6.65 -    input("Isar_Document.edit_version",
    6.66 -      Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
    6.67 -  }
    6.68 -}
     7.1 --- a/src/Pure/build-jars	Thu Aug 19 12:41:40 2010 +0200
     7.2 +++ b/src/Pure/build-jars	Thu Aug 19 12:51:48 2010 +0200
     7.3 @@ -41,6 +41,7 @@
     7.4    Isar/token.scala
     7.5    PIDE/command.scala
     7.6    PIDE/document.scala
     7.7 +  PIDE/isar_document.scala
     7.8    PIDE/markup_tree.scala
     7.9    PIDE/text.scala
    7.10    System/cygwin.scala
    7.11 @@ -50,7 +51,6 @@
    7.12    System/isabelle_process.scala
    7.13    System/isabelle_syntax.scala
    7.14    System/isabelle_system.scala
    7.15 -  System/isar_document.scala
    7.16    System/platform.scala
    7.17    System/session.scala
    7.18    System/session_manager.scala