propagate header changes to prover process;
authorwenzelm
Sun Jul 10 00:21:19 2011 +0200 (2011-07-10 ago)
changeset 437229b5dadb0c28d
parent 43721 fad8634cee62
child 43723 8a63c95b1d5b
propagate header changes to prover process;
simplified Document case classes;
Document.State.assignments: indexed by Version_ID;
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Jul 09 21:53:27 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Jul 10 00:21:19 2011 +0200
     1.3 @@ -16,12 +16,14 @@
     1.4    val parse_id: string -> id
     1.5    val print_id: id -> string
     1.6    type edit = string * ((command_id option * command_id option) list) option
     1.7 +  type header = string * (string * string list * string list)
     1.8    type state
     1.9    val init_state: state
    1.10    val get_theory: state -> version_id -> Position.T -> string -> theory
    1.11    val cancel_execution: state -> unit -> unit
    1.12    val define_command: command_id -> string -> state -> state
    1.13 -  val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
    1.14 +  val edit: version_id -> version_id -> edit list -> header list ->
    1.15 +    state -> (command_id * exec_id) list * state
    1.16    val execute: version_id -> state -> state
    1.17    val state: unit -> state
    1.18    val change_state: (state -> state) -> unit
    1.19 @@ -78,6 +80,8 @@
    1.20    (*NONE: remove node, SOME: insert/remove commands*)
    1.21    ((command_id option * command_id option) list) option;
    1.22  
    1.23 +type header = string * (string * string list * string list);
    1.24 +
    1.25  fun the_entry (Node {entries, ...}) id =
    1.26    (case Entries.lookup entries id of
    1.27      NONE => err_undef "command entry" id
    1.28 @@ -309,8 +313,10 @@
    1.29  
    1.30  in
    1.31  
    1.32 -fun edit (old_id: version_id) (new_id: version_id) edits state =
    1.33 +fun edit (old_id: version_id) (new_id: version_id) edits headers state =
    1.34    let
    1.35 +    (* FIXME apply headers *)
    1.36 +
    1.37      val old_version = the_version state old_id;
    1.38      val _ = Time.now ();  (* FIXME odd workaround *)
    1.39      val new_version = fold edit_nodes edits old_version;
     2.1 --- a/src/Pure/PIDE/document.scala	Sat Jul 09 21:53:27 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Sun Jul 10 00:21:19 2011 +0200
     2.3 @@ -70,11 +70,6 @@
     2.4      val blobs: Map[String, Blob],
     2.5      val commands: Linear_Set[Command])
     2.6    {
     2.7 -    /* header */
     2.8 -
     2.9 -    def set_header(new_header: Node.Header): Node = copy(header = new_header)
    2.10 -
    2.11 -
    2.12      /* commands */
    2.13  
    2.14      private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
    2.15 @@ -135,25 +130,24 @@
    2.16  
    2.17    object Version
    2.18    {
    2.19 -    val init: Version = new Version(no_id, Map().withDefaultValue(Node.empty))
    2.20 +    val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
    2.21    }
    2.22  
    2.23 -  class Version(val id: Version_ID, val nodes: Map[String, Node])
    2.24 +  sealed case class Version(val id: Version_ID, val nodes: Map[String, Node])
    2.25  
    2.26  
    2.27    /* changes of plain text, eventually resulting in document edits */
    2.28  
    2.29    object Change
    2.30    {
    2.31 -    val init = new Change(Future.value(Version.init), Nil, Future.value(Nil, Version.init))
    2.32 +    val init = Change(Future.value(Version.init), Nil, Future.value(Version.init))
    2.33    }
    2.34  
    2.35 -  class Change(
    2.36 +  sealed case class Change(
    2.37      val previous: Future[Version],
    2.38      val edits: List[Edit_Text],
    2.39 -    val result: Future[(List[Edit_Command], Version)])
    2.40 +    val version: Future[Version])
    2.41    {
    2.42 -    val version: Future[Version] = result.map(_._2)
    2.43      def is_finished: Boolean = previous.is_finished && version.is_finished
    2.44    }
    2.45  
    2.46 @@ -216,7 +210,7 @@
    2.47      val versions: Map[Version_ID, Version] = Map(),
    2.48      val commands: Map[Command_ID, Command.State] = Map(),
    2.49      val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
    2.50 -    val assignments: Map[Version, State.Assignment] = Map(),
    2.51 +    val assignments: Map[Version_ID, State.Assignment] = Map(),
    2.52      val disposed: Set[ID] = Set(),  // FIXME unused!?
    2.53      val history: History = History.init)
    2.54    {
    2.55 @@ -227,7 +221,7 @@
    2.56        val id = version.id
    2.57        if (versions.isDefinedAt(id) || disposed(id)) fail
    2.58        copy(versions = versions + (id -> version),
    2.59 -        assignments = assignments + (version -> State.Assignment(former_assignment)))
    2.60 +        assignments = assignments + (id -> State.Assignment(former_assignment)))
    2.61      }
    2.62  
    2.63      def define_command(command: Command): State =
    2.64 @@ -242,7 +236,8 @@
    2.65      def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
    2.66      def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
    2.67      def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
    2.68 -    def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
    2.69 +    def the_assignment(version: Version): State.Assignment =
    2.70 +      assignments.getOrElse(version.id, fail)
    2.71  
    2.72      def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
    2.73        execs.get(id) match {
    2.74 @@ -272,22 +267,21 @@
    2.75            (st.command, exec_id)
    2.76          }
    2.77        val new_assignment = the_assignment(version).assign(assigned_execs)
    2.78 -      val new_state =
    2.79 -        copy(assignments = assignments + (version -> new_assignment), execs = new_execs)
    2.80 +      val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
    2.81        (assigned_execs.map(_._1), new_state)
    2.82      }
    2.83  
    2.84      def is_assigned(version: Version): Boolean =
    2.85 -      assignments.get(version) match {
    2.86 +      assignments.get(version.id) match {
    2.87          case Some(assgn) => assgn.is_finished
    2.88          case None => false
    2.89        }
    2.90  
    2.91      def extend_history(previous: Future[Version],
    2.92          edits: List[Edit_Text],
    2.93 -        result: Future[(List[Edit_Command], Version)]): (Change, State) =
    2.94 +        version: Future[Version]): (Change, State) =
    2.95      {
    2.96 -      val change = new Change(previous, edits, result)
    2.97 +      val change = Change(previous, edits, version)
    2.98        (change, copy(history = history + change))
    2.99      }
   2.100  
     3.1 --- a/src/Pure/PIDE/isar_document.ML	Sat Jul 09 21:53:27 2011 +0200
     3.2 +++ b/src/Pure/PIDE/isar_document.ML	Sun Jul 10 00:21:19 2011 +0200
     3.3 @@ -13,7 +13,7 @@
     3.4  
     3.5  val _ =
     3.6    Isabelle_Process.add_command "Isar_Document.edit_version"
     3.7 -    (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
     3.8 +    (fn [old_id_string, new_id_string, edits_yxml, headers_yxml] => Document.change_state (fn state =>
     3.9        let
    3.10          val old_id = Document.parse_id old_id_string;
    3.11          val new_id = Document.parse_id new_id_string;
    3.12 @@ -26,9 +26,15 @@
    3.13                    (XML_Data.dest_pair
    3.14                      (XML_Data.dest_option XML_Data.dest_int)
    3.15                      (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
    3.16 +        val headers =
    3.17 +          XML_Data.dest_list
    3.18 +            (XML_Data.dest_pair XML_Data.dest_string
    3.19 +              (XML_Data.dest_triple XML_Data.dest_string
    3.20 +                (XML_Data.dest_list XML_Data.dest_string)
    3.21 +                (XML_Data.dest_list XML_Data.dest_string))) (YXML.parse_body headers_yxml);
    3.22  
    3.23        val await_cancellation = Document.cancel_execution state;
    3.24 -      val (updates, state') = Document.edit old_id new_id edits state;
    3.25 +      val (updates, state') = Document.edit old_id new_id edits headers state;
    3.26        val _ = await_cancellation ();
    3.27        val _ =
    3.28          Output.status (Markup.markup (Markup.assign new_id)
     4.1 --- a/src/Pure/PIDE/isar_document.scala	Sat Jul 09 21:53:27 2011 +0200
     4.2 +++ b/src/Pure/PIDE/isar_document.scala	Sun Jul 10 00:21:19 2011 +0200
     4.3 @@ -140,9 +140,9 @@
     4.4    /* document versions */
     4.5  
     4.6    def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
     4.7 -      edits: List[Document.Edit_Command_ID])
     4.8 +      edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
     4.9    {
    4.10 -    val arg =
    4.11 +    val arg1 =
    4.12        XML_Data.make_list(
    4.13          XML_Data.make_pair(XML_Data.make_string)(
    4.14            XML_Data.make_option(XML_Data.make_list(
    4.15 @@ -150,7 +150,11 @@
    4.16                  XML_Data.make_option(XML_Data.make_long))(
    4.17                  XML_Data.make_option(XML_Data.make_long))))))(edits)
    4.18  
    4.19 +    val arg2 =
    4.20 +      XML_Data.make_list(XML_Data.make_pair(XML_Data.make_string)(Thy_Header.make_xml_data))(headers)
    4.21 +
    4.22      input("Isar_Document.edit_version",
    4.23 -      Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
    4.24 +      Document.ID(old_id), Document.ID(new_id),
    4.25 +        YXML.string_of_body(arg1), YXML.string_of_body(arg2))
    4.26    }
    4.27  }
     5.1 --- a/src/Pure/System/session.scala	Sat Jul 09 21:53:27 2011 +0200
     5.2 +++ b/src/Pure/System/session.scala	Sun Jul 10 00:21:19 2011 +0200
     5.3 @@ -165,7 +165,12 @@
     5.4    private case object Interrupt
     5.5    private case class Init_Node(name: String, header: Document.Node.Header, text: String)
     5.6    private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
     5.7 -  private case class Change_Node(name: String, header: Document.Node.Header, change: Document.Change)
     5.8 +  private case class Change_Node(
     5.9 +    name: String,
    5.10 +    doc_edits: List[Document.Edit_Command],
    5.11 +    header_edits: List[(String, Thy_Header.Header)],
    5.12 +    previous: Document.Version,
    5.13 +    version: Document.Version)
    5.14  
    5.15    private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
    5.16    {
    5.17 @@ -182,27 +187,36 @@
    5.18        val syntax = current_syntax()
    5.19        val previous = global_state().history.tip.version
    5.20        val doc_edits = edits.map(edit => (name, edit))
    5.21 -      val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
    5.22 -      val change = global_state.change_yield(_.extend_history(previous, doc_edits, result))
    5.23 +      val result = Future.fork {
    5.24 +        Thy_Syntax.text_edits(syntax, previous.join, doc_edits, List((name, header)))
    5.25 +      }
    5.26 +      val change =
    5.27 +        global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._3)))
    5.28  
    5.29 -      change.version.map(_ => {
    5.30 -        assignments.await { global_state().is_assigned(previous.get_finished) }
    5.31 -        this_actor ! Change_Node(name, header, change) })
    5.32 +      result.map {
    5.33 +        case (doc_edits, header_edits, _) =>
    5.34 +          assignments.await { global_state().is_assigned(previous.get_finished) }
    5.35 +          this_actor !
    5.36 +            Change_Node(name, doc_edits, header_edits, previous.join, change.version.join)
    5.37 +      }
    5.38      }
    5.39      //}}}
    5.40  
    5.41  
    5.42      /* resulting changes */
    5.43  
    5.44 -    def handle_change(name: String, header: Document.Node.Header, change: Document.Change)
    5.45 +    def handle_change(change: Change_Node)
    5.46      //{{{
    5.47      {
    5.48 -      val previous = change.previous.get_finished
    5.49 -      val (node_edits, version) = change.result.get_finished
    5.50 +      val previous = change.previous
    5.51 +      val version = change.version
    5.52 +      val name = change.name
    5.53 +      val doc_edits = change.doc_edits
    5.54 +      val header_edits = change.header_edits
    5.55  
    5.56        var former_assignment = global_state().the_assignment(previous).get_finished
    5.57        for {
    5.58 -        (name, Some(cmd_edits)) <- node_edits
    5.59 +        (name, Some(cmd_edits)) <- doc_edits
    5.60          (prev, None) <- cmd_edits
    5.61          removed <- previous.nodes(name).commands.get_after(prev)
    5.62        } former_assignment -= removed
    5.63 @@ -216,14 +230,15 @@
    5.64          command.id
    5.65        }
    5.66        val id_edits =
    5.67 -        node_edits map {
    5.68 +        doc_edits map {
    5.69            case (name, edits) =>
    5.70              val ids =
    5.71                edits.map(_.map { case (c1, c2) => (c1.map(id_command), c2.map(id_command)) })
    5.72              (name, ids)
    5.73          }
    5.74 +
    5.75        global_state.change(_.define_version(version, former_assignment))
    5.76 -      prover.get.edit_version(previous.id, version.id, id_edits)
    5.77 +      prover.get.edit_version(previous.id, version.id, id_edits, header_edits)
    5.78      }
    5.79      //}}}
    5.80  
    5.81 @@ -315,8 +330,8 @@
    5.82            handle_edits(name, header, List(Some(text_edits)))
    5.83            reply(())
    5.84  
    5.85 -        case Change_Node(name, header, change) if prover.isDefined =>
    5.86 -          handle_change(name, header, change)
    5.87 +        case change: Change_Node if prover.isDefined =>
    5.88 +          handle_change(change)
    5.89  
    5.90          case input: Isabelle_Process.Input =>
    5.91            raw_messages.event(input)
     6.1 --- a/src/Pure/Thy/thy_header.scala	Sat Jul 09 21:53:27 2011 +0200
     6.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 00:21:19 2011 +0200
     6.3 @@ -31,6 +31,11 @@
     6.4        Header(f(name), imports.map(f), uses.map(f))
     6.5    }
     6.6  
     6.7 +  def make_xml_data(header: Header): XML.Body =
     6.8 +    XML_Data.make_triple(XML_Data.make_string)(
     6.9 +      XML_Data.make_list(XML_Data.make_string))(
    6.10 +        XML_Data.make_list(XML_Data.make_string))(header.name, header.imports, header.uses)
    6.11 +
    6.12  
    6.13    /* file name */
    6.14  
     7.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Jul 09 21:53:27 2011 +0200
     7.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun Jul 10 00:21:19 2011 +0200
     7.3 @@ -99,8 +99,12 @@
     7.4  
     7.5    /** text edits **/
     7.6  
     7.7 -  def text_edits(syntax: Outer_Syntax, previous: Document.Version,
     7.8 -      edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
     7.9 +  def text_edits(
    7.10 +      syntax: Outer_Syntax,
    7.11 +      previous: Document.Version,
    7.12 +      edits: List[Document.Edit_Text],
    7.13 +      headers: List[(String, Document.Node.Header)])
    7.14 +    : (List[Document.Edit_Command], List[(String, Thy_Header.Header)], Document.Version) =
    7.15    {
    7.16      /* phase 1: edit individual command source */
    7.17  
    7.18 @@ -169,10 +173,25 @@
    7.19      }
    7.20  
    7.21  
    7.22 +    /* node header */
    7.23 +
    7.24 +    def node_header(name: String, node: Document.Node)
    7.25 +        : (List[(String, Thy_Header.Header)], Document.Node.Header) =
    7.26 +      (node.header.thy_header, headers.find(p => p._1 == name).map(_._2)) match {
    7.27 +        case (Exn.Res(thy_header0), Some(header @ Document.Node.Header(_, Exn.Res(thy_header))))
    7.28 +        if thy_header0 != thy_header =>
    7.29 +          (List((name, thy_header)), header)
    7.30 +        case (Exn.Exn(_), Some(header @ Document.Node.Header(_, Exn.Res(thy_header)))) =>
    7.31 +          (List((name, thy_header)), header)
    7.32 +        case _ => (Nil, node.header)
    7.33 +      }
    7.34 +
    7.35 +
    7.36      /* resulting document edits */
    7.37  
    7.38      {
    7.39        val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
    7.40 +      val header_edits = new mutable.ListBuffer[(String, Thy_Header.Header)]
    7.41        var nodes = previous.nodes
    7.42  
    7.43        edits foreach {
    7.44 @@ -194,9 +213,13 @@
    7.45              inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
    7.46  
    7.47            doc_edits += (name -> Some(cmd_edits))
    7.48 -          nodes += (name -> Document.Node(node.header, node.blobs, commands2))
    7.49 +
    7.50 +          val (new_headers, new_header) = node_header(name, node)
    7.51 +          header_edits ++= new_headers
    7.52 +
    7.53 +          nodes += (name -> Document.Node(new_header, node.blobs, commands2))
    7.54        }
    7.55 -      (doc_edits.toList, new Document.Version(Document.new_id(), nodes))
    7.56 +      (doc_edits.toList, header_edits.toList, Document.Version(Document.new_id(), nodes))
    7.57      }
    7.58    }
    7.59  }
     8.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Jul 09 21:53:27 2011 +0200
     8.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Jul 10 00:21:19 2011 +0200
     8.3 @@ -64,7 +64,7 @@
     8.4    private val node_name = (master_dir + Path.basic(thy_name)).implode
     8.5  
     8.6    private def node_header(): Document.Node.Header =
     8.7 -    Document.Node.Header(master_dir,
     8.8 +    Document.Node.Header(Path.current,  // FIXME master_dir (!?)
     8.9        Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
    8.10  
    8.11    private object pending_edits  // owned by Swing thread