clarified node header -- exclude master_dir;
authorwenzelm
Sat Aug 13 15:59:26 2011 +0200 (2011-08-13)
changeset 44182ecb51b457064
parent 44181 bbce0417236d
child 44183 1de22a7b2a82
clarified node header -- exclude master_dir;
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_syntax.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Aug 13 13:48:26 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Aug 13 15:59:26 2011 +0200
     1.3 @@ -15,11 +15,11 @@
     1.4    val new_id: unit -> id
     1.5    val parse_id: string -> id
     1.6    val print_id: id -> string
     1.7 -  type node_header = string * string list * string list
     1.8 +  type node_header = (string * string list * string list) Exn.result
     1.9    datatype node_edit =
    1.10      Remove |
    1.11      Edits of (command_id option * command_id option) list |
    1.12 -    Update_Header of node_header Exn.result
    1.13 +    Header of node_header
    1.14    type edit = string * node_edit
    1.15    type state
    1.16    val init_state: state
    1.17 @@ -55,11 +55,11 @@
    1.18  
    1.19  (** document structure **)
    1.20  
    1.21 -type node_header = string * string list * string list;
    1.22 +type node_header = (string * string list * string list) Exn.result;
    1.23  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    1.24  
    1.25  abstype node = Node of
    1.26 - {header: node_header Exn.result,
    1.27 + {header: node_header,
    1.28    entries: exec_id option Entries.T,  (*command entries with excecutions*)
    1.29    last: exec_id}  (*last entry with main result*)
    1.30  and version = Version of node Graph.T  (*development graph wrt. static imports*)
    1.31 @@ -90,7 +90,7 @@
    1.32  datatype node_edit =
    1.33    Remove |
    1.34    Edits of (command_id option * command_id option) list |
    1.35 -  Update_Header of node_header Exn.result;
    1.36 +  Header of node_header;
    1.37  
    1.38  type edit = string * node_edit;
    1.39  
    1.40 @@ -129,7 +129,7 @@
    1.41        Remove => perhaps (try (Graph.del_node name)) nodes
    1.42      | Edits edits => update_node name (edit_node edits) nodes
    1.43      (* FIXME maintain deps; cycles!? *)
    1.44 -    | Update_Header header => update_node name (set_header header) nodes);
    1.45 +    | Header header => update_node name (set_header header) nodes);
    1.46  
    1.47  fun put_node name node (Version nodes) =
    1.48    Version (nodes
     2.1 --- a/src/Pure/PIDE/document.scala	Sat Aug 13 13:48:26 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Sat Aug 13 15:59:26 2011 +0200
     2.3 @@ -36,6 +36,8 @@
     2.4    type Edit_Command = Edit[(Option[Command], Option[Command])]
     2.5    type Edit_Command_ID = Edit[(Option[Command_ID], Option[Command_ID])]
     2.6  
     2.7 +  type Node_Header = Exn.Result[Thy_Header]
     2.8 +
     2.9    object Node
    2.10    {
    2.11      sealed abstract class Edit[A]
    2.12 @@ -44,26 +46,20 @@
    2.13          this match {
    2.14            case Remove() => Remove()
    2.15            case Edits(es) => Edits(es.map(f))
    2.16 -          case Update_Header(header: Header) => Update_Header(header)
    2.17 +          case Header(header) => Header(header)
    2.18          }
    2.19      }
    2.20      case class Remove[A]() extends Edit[A]
    2.21      case class Edits[A](edits: List[A]) extends Edit[A]
    2.22 -    case class Update_Header[A](header: Header) extends Edit[A]
    2.23 +    case class Header[A](header: Node_Header) extends Edit[A]
    2.24  
    2.25 -    sealed case class Header(val master_dir: String, val thy_header: Exn.Result[Thy_Header])
    2.26 -    {
    2.27 -      def norm_deps(f: (String, Path) => String): Header =
    2.28 -        copy(thy_header =
    2.29 -          thy_header match {
    2.30 -            case Exn.Res(header) =>
    2.31 -              Exn.capture { header.norm_deps(name => f(master_dir, Path.explode(name))) }
    2.32 -            case exn => exn
    2.33 -          })
    2.34 -    }
    2.35 -    val empty_header = Header("", Exn.Exn(ERROR("Bad theory header")))
    2.36 +    def norm_header[A](f: Path => String, header: Node_Header): Header[A] =
    2.37 +      header match {
    2.38 +        case Exn.Res(h) => Header[A](Exn.capture { h.norm_deps(name => f(Path.explode(name))) })
    2.39 +        case exn => Header[A](exn)
    2.40 +      }
    2.41  
    2.42 -    val empty: Node = Node(empty_header, Map(), Linear_Set())
    2.43 +    val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Map(), Linear_Set())
    2.44  
    2.45      def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
    2.46        : Iterator[(Command, Text.Offset)] =
    2.47 @@ -80,7 +76,7 @@
    2.48    private val block_size = 1024
    2.49  
    2.50    sealed case class Node(
    2.51 -    val header: Node.Header,
    2.52 +    val header: Node_Header,
    2.53      val blobs: Map[String, Blob],
    2.54      val commands: Linear_Set[Command])
    2.55    {
     3.1 --- a/src/Pure/PIDE/isar_document.ML	Sat Aug 13 13:48:26 2011 +0200
     3.2 +++ b/src/Pure/PIDE/isar_document.ML	Sat Aug 13 15:59:26 2011 +0200
     3.3 @@ -25,8 +25,8 @@
     3.4                   [fn ([], []) => Document.Remove,
     3.5                    fn ([], a) => Document.Edits (list (pair (option int) (option int)) a),
     3.6                    fn ([], a) =>
     3.7 -                    Document.Update_Header (Exn.Res (triple string (list string) (list string) a)),
     3.8 -                  fn ([a], []) => Document.Update_Header (Exn.Exn (ERROR a))]))
     3.9 +                    Document.Header (Exn.Res (triple string (list string) (list string) a)),
    3.10 +                  fn ([a], []) => Document.Header (Exn.Exn (ERROR a))]))
    3.11              end;
    3.12  
    3.13        val await_cancellation = Document.cancel_execution state;
     4.1 --- a/src/Pure/PIDE/isar_document.scala	Sat Aug 13 13:48:26 2011 +0200
     4.2 +++ b/src/Pure/PIDE/isar_document.scala	Sat Aug 13 15:59:26 2011 +0200
     4.3 @@ -149,11 +149,9 @@
     4.4            variant(List(
     4.5              { case Document.Node.Remove() => (Nil, Nil) },
     4.6              { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
     4.7 -            { case Document.Node.Update_Header(
     4.8 -                  Document.Node.Header(_, Exn.Res(Thy_Header(a, b, c)))) =>
     4.9 +            { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
    4.10                  (Nil, triple(string, list(string), list(string))(a, b, c)) },
    4.11 -            { case Document.Node.Update_Header(
    4.12 -                  Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))
    4.13 +            { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }))))
    4.14        YXML.string_of_body(encode(edits)) }
    4.15  
    4.16      input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
     5.1 --- a/src/Pure/System/session.scala	Sat Aug 13 13:48:26 2011 +0200
     5.2 +++ b/src/Pure/System/session.scala	Sat Aug 13 15:59:26 2011 +0200
     5.3 @@ -164,8 +164,10 @@
     5.4  
     5.5    private case class Start(timeout: Time, args: List[String])
     5.6    private case object Interrupt
     5.7 -  private case class Init_Node(name: String, header: Document.Node.Header, text: String)
     5.8 -  private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
     5.9 +  private case class Init_Node(
    5.10 +    name: String, master_dir: String, header: Document.Node_Header, text: String)
    5.11 +  private case class Edit_Node(
    5.12 +    name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
    5.13    private case class Change_Node(
    5.14      name: String,
    5.15      doc_edits: List[Document.Edit_Command],
    5.16 @@ -180,15 +182,15 @@
    5.17  
    5.18      /* incoming edits */
    5.19  
    5.20 -    def handle_edits(name: String,
    5.21 -        header: Document.Node.Header, edits: List[Document.Node.Edit[Text.Edit]])
    5.22 +    def handle_edits(name: String, master_dir: String,
    5.23 +        header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit]])
    5.24      //{{{
    5.25      {
    5.26        val syntax = current_syntax()
    5.27        val previous = global_state().history.tip.version
    5.28 -      val doc_edits =
    5.29 -        (name, Document.Node.Update_Header[Text.Edit](header.norm_deps(file_store.append))) ::
    5.30 -          edits.map(edit => (name, edit))
    5.31 +      val norm_header =
    5.32 +        Document.Node.norm_header[Text.Edit](file_store.append(master_dir, _), header)
    5.33 +      val doc_edits = (name, norm_header) :: edits.map(edit => (name, edit))
    5.34        val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
    5.35        val change =
    5.36          global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2)))
    5.37 @@ -325,14 +327,14 @@
    5.38          case Interrupt if prover.isDefined =>
    5.39            prover.get.interrupt
    5.40  
    5.41 -        case Init_Node(name, header, text) if prover.isDefined =>
    5.42 +        case Init_Node(name, master_dir, header, text) if prover.isDefined =>
    5.43            // FIXME compare with existing node
    5.44 -          handle_edits(name, header,
    5.45 +          handle_edits(name, master_dir, header,
    5.46              List(Document.Node.Remove(), Document.Node.Edits(List(Text.Edit.insert(0, text)))))
    5.47            reply(())
    5.48  
    5.49 -        case Edit_Node(name, header, text_edits) if prover.isDefined =>
    5.50 -          handle_edits(name, header, List(Document.Node.Edits(text_edits)))
    5.51 +        case Edit_Node(name, master_dir, header, text_edits) if prover.isDefined =>
    5.52 +          handle_edits(name, master_dir, header, List(Document.Node.Edits(text_edits)))
    5.53            reply(())
    5.54  
    5.55          case change: Change_Node if prover.isDefined =>
    5.56 @@ -360,9 +362,9 @@
    5.57  
    5.58    def interrupt() { session_actor ! Interrupt }
    5.59  
    5.60 -  def init_node(name: String, header: Document.Node.Header, text: String)
    5.61 -  { session_actor !? Init_Node(name, header, text) }
    5.62 +  def init_node(name: String, master_dir: String, header: Document.Node_Header, text: String)
    5.63 +  { session_actor !? Init_Node(name, master_dir, header, text) }
    5.64  
    5.65 -  def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
    5.66 -  { session_actor !? Edit_Node(name, header, edits) }
    5.67 +  def edit_node(name: String, master_dir: String, header: Document.Node_Header, edits: List[Text.Edit])
    5.68 +  { session_actor !? Edit_Node(name, master_dir, header, edits) }
    5.69  }
     6.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 13:48:26 2011 +0200
     6.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 13 15:59:26 2011 +0200
     6.3 @@ -199,16 +199,15 @@
     6.4            doc_edits += (name -> Document.Node.Edits(cmd_edits))
     6.5            nodes += (name -> node.copy(commands = commands2))
     6.6  
     6.7 -        case (name, Document.Node.Update_Header(header)) =>
     6.8 +        case (name, Document.Node.Header(header)) =>
     6.9            val node = nodes(name)
    6.10            val update_header =
    6.11 -            (node.header.thy_header, header) match {
    6.12 -              case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header))) =>
    6.13 -                thy_header0 != thy_header
    6.14 +            (node.header, header) match {
    6.15 +              case (Exn.Res(thy_header0), Exn.Res(thy_header)) => thy_header0 != thy_header
    6.16                case _ => true
    6.17              }
    6.18            if (update_header) {
    6.19 -            doc_edits += (name -> Document.Node.Update_Header(header))
    6.20 +            doc_edits += (name -> Document.Node.Header(header))
    6.21              nodes += (name -> node.copy(header = header))
    6.22            }
    6.23        }
     7.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Aug 13 13:48:26 2011 +0200
     7.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Aug 13 15:59:26 2011 +0200
     7.3 @@ -62,9 +62,8 @@
     7.4  {
     7.5    /* pending text edits */
     7.6  
     7.7 -  def node_header(): Document.Node.Header =
     7.8 -    Document.Node.Header(master_dir,
     7.9 -      Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
    7.10 +  def node_header(): Exn.Result[Thy_Header] =
    7.11 +    Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
    7.12  
    7.13    private object pending_edits  // owned by Swing thread
    7.14    {
    7.15 @@ -78,14 +77,14 @@
    7.16          case Nil =>
    7.17          case edits =>
    7.18            pending.clear
    7.19 -          session.edit_node(node_name, node_header(), edits)
    7.20 +          session.edit_node(node_name, master_dir, node_header(), edits)
    7.21        }
    7.22      }
    7.23  
    7.24      def init()
    7.25      {
    7.26        flush()
    7.27 -      session.init_node(node_name, node_header(), Isabelle.buffer_text(buffer))
    7.28 +      session.init_node(node_name, master_dir, node_header(), Isabelle.buffer_text(buffer))
    7.29      }
    7.30  
    7.31      private val delay_flush =