more abstract Document.Node.Name;
authorwenzelm
Thu Sep 01 13:34:45 2011 +0200 (2011-09-01 ago)
changeset 44615a4ff8a787202
parent 44614 466ea227e00d
child 44616 4beeaf2a226d
more abstract Document.Node.Name;
tuned signature;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/isar_document.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_load.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle_hyperlinks.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit_thy_load.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Sep 01 11:33:44 2011 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Sep 01 13:34:45 2011 +0200
     1.3 @@ -80,9 +80,10 @@
     1.4    /* dummy commands */
     1.5  
     1.6    def unparsed(source: String): Command =
     1.7 -    new Command(Document.no_id, "", List(Token(Token.Kind.UNPARSED, source)))
     1.8 +    new Command(Document.no_id, Document.Node.Name("", "", ""),
     1.9 +      List(Token(Token.Kind.UNPARSED, source)))
    1.10  
    1.11 -  def span(node_name: String, toks: List[Token]): Command =
    1.12 +  def span(node_name: Document.Node.Name, toks: List[Token]): Command =
    1.13      new Command(Document.no_id, node_name, toks)
    1.14  
    1.15  
    1.16 @@ -110,7 +111,7 @@
    1.17  
    1.18  class Command(
    1.19      val id: Document.Command_ID,
    1.20 -    val node_name: String,
    1.21 +    val node_name: Document.Node.Name,
    1.22      val span: List[Token])
    1.23  {
    1.24    /* classification */
     2.1 --- a/src/Pure/PIDE/document.scala	Thu Sep 01 11:33:44 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Thu Sep 01 13:34:45 2011 +0200
     2.3 @@ -31,7 +31,7 @@
     2.4  
     2.5    /* named nodes -- development graph */
     2.6  
     2.7 -  type Edit[A, B] = (String, Node.Edit[A, B])
     2.8 +  type Edit[A, B] = (Node.Name, Node.Edit[A, B])
     2.9    type Edit_Text = Edit[Text.Edit, Text.Perspective]
    2.10    type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
    2.11  
    2.12 @@ -39,6 +39,16 @@
    2.13  
    2.14    object Node
    2.15    {
    2.16 +    sealed case class Name(node: String, master_dir: String, theory: String)
    2.17 +    {
    2.18 +      override def hashCode: Int = node.hashCode
    2.19 +      override def equals(that: Any): Boolean =
    2.20 +        that match {
    2.21 +          case other: Name => node == other.node
    2.22 +          case _ => false
    2.23 +        }
    2.24 +    }
    2.25 +
    2.26      sealed abstract class Edit[A, B]
    2.27      {
    2.28        def foreach(f: A => Unit)
    2.29 @@ -149,7 +159,7 @@
    2.30      val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
    2.31    }
    2.32  
    2.33 -  type Nodes = Map[String, Node]
    2.34 +  type Nodes = Map[Node.Name, Node]
    2.35    sealed case class Version(val id: Version_ID, val nodes: Nodes)
    2.36  
    2.37  
    2.38 @@ -335,10 +345,10 @@
    2.39      def tip_stable: Boolean = is_stable(history.tip)
    2.40      def tip_version: Version = history.tip.version.get_finished
    2.41  
    2.42 -    def last_exec_offset(name: String): Text.Offset =
    2.43 +    def last_exec_offset(name: Node.Name): Text.Offset =
    2.44      {
    2.45        val version = tip_version
    2.46 -      the_assignment(version).last_execs.get(name) match {
    2.47 +      the_assignment(version).last_execs.get(name.node) match {
    2.48          case Some(Some(id)) =>
    2.49            val node = version.nodes(name)
    2.50            val cmd = the_command(id).command
    2.51 @@ -371,7 +381,7 @@
    2.52  
    2.53  
    2.54      // persistent user-view
    2.55 -    def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
    2.56 +    def snapshot(name: Node.Name, pending_edits: List[Text.Edit]): Snapshot =
    2.57      {
    2.58        val stable = recent_stable.get
    2.59        val latest = history.tip
     3.1 --- a/src/Pure/PIDE/isar_document.scala	Thu Sep 01 11:33:44 2011 +0200
     3.2 +++ b/src/Pure/PIDE/isar_document.scala	Thu Sep 01 13:34:45 2011 +0200
     3.3 @@ -160,14 +160,14 @@
     3.4    }
     3.5  
     3.6    def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
     3.7 -    name: String, perspective: Command.Perspective)
     3.8 +    name: Document.Node.Name, perspective: Command.Perspective)
     3.9    {
    3.10      val ids =
    3.11      { import XML.Encode._
    3.12        list(long)(perspective.commands.map(_.id)) }
    3.13  
    3.14 -    input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), name,
    3.15 -      YXML.string_of_body(ids))
    3.16 +    input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id),
    3.17 +      name.node, YXML.string_of_body(ids))
    3.18    }
    3.19  
    3.20    def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
    3.21 @@ -177,7 +177,7 @@
    3.22      { import XML.Encode._
    3.23        def id: T[Command] = (cmd => long(cmd.id))
    3.24        def encode: T[List[Document.Edit_Command]] =
    3.25 -        list(pair(string,
    3.26 +        list(pair((name => string(name.node)),
    3.27            variant(List(
    3.28              { case Document.Node.Clear() => (Nil, Nil) },
    3.29              { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
     4.1 --- a/src/Pure/System/session.scala	Thu Sep 01 11:33:44 2011 +0200
     4.2 +++ b/src/Pure/System/session.scala	Thu Sep 01 13:34:45 2011 +0200
     4.3 @@ -22,7 +22,7 @@
     4.4    case object Global_Settings
     4.5    case object Perspective
     4.6    case object Assignment
     4.7 -  case class Commands_Changed(nodes: Set[String], commands: Set[Command])
     4.8 +  case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command])
     4.9  
    4.10    sealed abstract class Phase
    4.11    case object Inactive extends Phase
    4.12 @@ -63,7 +63,7 @@
    4.13    private val (_, command_change_buffer) =
    4.14      Simple_Thread.actor("command_change_buffer", daemon = true)
    4.15    {
    4.16 -    var changed_nodes: Set[String] = Set.empty
    4.17 +    var changed_nodes: Set[Document.Node.Name] = Set.empty
    4.18      var changed_commands: Set[Command] = Set.empty
    4.19      def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty
    4.20  
    4.21 @@ -134,23 +134,22 @@
    4.22    private val global_state = new Volatile(Document.State.init)
    4.23    def current_state(): Document.State = global_state()
    4.24  
    4.25 -  def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
    4.26 +  def snapshot(name: Document.Node.Name, pending_edits: List[Text.Edit]): Document.Snapshot =
    4.27      global_state().snapshot(name, pending_edits)
    4.28  
    4.29  
    4.30    /* theory files */
    4.31  
    4.32 -  def header_edit(name: String, master_dir: String,
    4.33 -    header: Document.Node_Header): Document.Edit_Text =
    4.34 +  def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text =
    4.35    {
    4.36      def norm_import(s: String): String =
    4.37      {
    4.38        val thy_name = Thy_Header.base_name(s)
    4.39        if (thy_load.is_loaded(thy_name)) thy_name
    4.40 -      else thy_load.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
    4.41 +      else thy_load.append(name.master_dir, Thy_Header.thy_path(Path.explode(s)))
    4.42      }
    4.43      def norm_use(s: String): String =
    4.44 -      thy_load.append(master_dir, Path.explode(s))
    4.45 +      thy_load.append(name.master_dir, Path.explode(s))
    4.46  
    4.47      val header1: Document.Node_Header =
    4.48        header match {
    4.49 @@ -167,12 +166,12 @@
    4.50  
    4.51    private case class Start(timeout: Time, args: List[String])
    4.52    private case object Interrupt
    4.53 -  private case class Init_Node(name: String, master_dir: String,
    4.54 +  private case class Init_Node(name: Document.Node.Name,
    4.55      header: Document.Node_Header, perspective: Text.Perspective, text: String)
    4.56 -  private case class Edit_Node(name: String, master_dir: String,
    4.57 +  private case class Edit_Node(name: Document.Node.Name,
    4.58      header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
    4.59    private case class Change_Node(
    4.60 -    name: String,
    4.61 +    name: Document.Node.Name,
    4.62      doc_edits: List[Document.Edit_Command],
    4.63      previous: Document.Version,
    4.64      version: Document.Version)
    4.65 @@ -185,7 +184,7 @@
    4.66  
    4.67      /* perspective */
    4.68  
    4.69 -    def update_perspective(name: String, text_perspective: Text.Perspective)
    4.70 +    def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective)
    4.71      {
    4.72        val previous = global_state().tip_version
    4.73        val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
    4.74 @@ -206,7 +205,7 @@
    4.75  
    4.76      /* incoming edits */
    4.77  
    4.78 -    def handle_edits(name: String, master_dir: String,
    4.79 +    def handle_edits(name: Document.Node.Name,
    4.80          header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
    4.81      //{{{
    4.82      {
    4.83 @@ -215,7 +214,7 @@
    4.84  
    4.85        prover.get.cancel_execution()
    4.86  
    4.87 -      val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit))
    4.88 +      val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
    4.89        val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
    4.90        val change =
    4.91          global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2)))
    4.92 @@ -354,20 +353,20 @@
    4.93          case Interrupt if prover.isDefined =>
    4.94            prover.get.interrupt
    4.95  
    4.96 -        case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined =>
    4.97 +        case Init_Node(name, header, perspective, text) if prover.isDefined =>
    4.98            // FIXME compare with existing node
    4.99 -          handle_edits(name, master_dir, header,
   4.100 +          handle_edits(name, header,
   4.101              List(Document.Node.Clear(),
   4.102                Document.Node.Edits(List(Text.Edit.insert(0, text))),
   4.103                Document.Node.Perspective(perspective)))
   4.104            reply(())
   4.105  
   4.106 -        case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
   4.107 +        case Edit_Node(name, header, perspective, text_edits) if prover.isDefined =>
   4.108            if (text_edits.isEmpty && global_state().tip_stable &&
   4.109                perspective.range.stop <= global_state().last_exec_offset(name))
   4.110              update_perspective(name, perspective)
   4.111            else
   4.112 -            handle_edits(name, master_dir, header,
   4.113 +            handle_edits(name, header,
   4.114                List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
   4.115            reply(())
   4.116  
   4.117 @@ -396,13 +395,11 @@
   4.118  
   4.119    def interrupt() { session_actor ! Interrupt }
   4.120  
   4.121 -  // FIXME simplify signature
   4.122 -  def init_node(name: String, master_dir: String,
   4.123 +  def init_node(name: Document.Node.Name,
   4.124      header: Document.Node_Header, perspective: Text.Perspective, text: String)
   4.125 -  { session_actor !? Init_Node(name, master_dir, header, perspective, text) }
   4.126 +  { session_actor !? Init_Node(name, header, perspective, text) }
   4.127  
   4.128 -  // FIXME simplify signature
   4.129 -  def edit_node(name: String, master_dir: String, header: Document.Node_Header,
   4.130 -    perspective: Text.Perspective, edits: List[Text.Edit])
   4.131 -  { session_actor !? Edit_Node(name, master_dir, header, perspective, edits) }
   4.132 +  def edit_node(name: Document.Node.Name,
   4.133 +    header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
   4.134 +  { session_actor !? Edit_Node(name, header, perspective, edits) }
   4.135  }
     5.1 --- a/src/Pure/Thy/thy_info.scala	Thu Sep 01 11:33:44 2011 +0200
     5.2 +++ b/src/Pure/Thy/thy_info.scala	Thu Sep 01 13:34:45 2011 +0200
     5.3 @@ -25,51 +25,54 @@
     5.4  {
     5.5    /* messages */
     5.6  
     5.7 -  private def show_path(names: List[String]): String =
     5.8 -    names.map(quote).mkString(" via ")
     5.9 +  private def show_path(names: List[Document.Node.Name]): String =
    5.10 +    names.map(name => quote(name.theory)).mkString(" via ")
    5.11  
    5.12 -  private def cycle_msg(names: List[String]): String =
    5.13 +  private def cycle_msg(names: List[Document.Node.Name]): String =
    5.14      "Cyclic dependency of " + show_path(names)
    5.15  
    5.16 -  private def required_by(s: String, initiators: List[String]): String =
    5.17 +  private def required_by(initiators: List[Document.Node.Name]): String =
    5.18      if (initiators.isEmpty) ""
    5.19 -    else s + "(required by " + show_path(initiators.reverse) + ")"
    5.20 +    else "\n(required by " + show_path(initiators.reverse) + ")"
    5.21  
    5.22  
    5.23    /* dependencies */
    5.24  
    5.25 -  type Deps = Map[String, Document.Node_Header]
    5.26 -
    5.27 -  private def require_thys(initiators: List[String],
    5.28 -      deps: Deps, thys: List[(String, String)]): Deps =
    5.29 -    (deps /: thys)(require_thy(initiators, _, _))
    5.30 -
    5.31 -  private def require_thy(initiators: List[String], deps: Deps, thy: (String, String)): Deps =
    5.32 +  def import_name(master_dir: String, str: String): Document.Node.Name =
    5.33    {
    5.34 -    val (dir, str) = thy
    5.35      val path = Path.explode(str)
    5.36 -    val thy_name = path.base.implode
    5.37 -    val node_name = thy_load.append(dir, Thy_Header.thy_path(path))
    5.38 +    val node_name = thy_load.append(master_dir, Thy_Header.thy_path(path))
    5.39 +    val master_dir1 = thy_load.append(master_dir, path.dir)
    5.40 +    Document.Node.Name(node_name, master_dir1, path.base.implode)
    5.41 +  }
    5.42 +
    5.43 +  type Deps = Map[Document.Node.Name, Document.Node_Header]
    5.44  
    5.45 -    if (deps.isDefinedAt(node_name) || thy_load.is_loaded(thy_name)) deps
    5.46 +  private def require_thys(initiators: List[Document.Node.Name],
    5.47 +      deps: Deps, names: List[Document.Node.Name]): Deps =
    5.48 +    (deps /: names)(require_thy(initiators, _, _))
    5.49 +
    5.50 +  private def require_thy(initiators: List[Document.Node.Name],
    5.51 +      deps: Deps, name: Document.Node.Name): Deps =
    5.52 +  {
    5.53 +    if (deps.isDefinedAt(name) || thy_load.is_loaded(name.theory)) deps
    5.54      else {
    5.55 -      val dir1 = thy_load.append(dir, path.dir)
    5.56        try {
    5.57 -        if (initiators.contains(node_name)) error(cycle_msg(initiators))
    5.58 +        if (initiators.contains(name)) error(cycle_msg(initiators))
    5.59          val header =
    5.60 -          try { thy_load.check_thy(node_name) }
    5.61 +          try { thy_load.check_thy(name) }
    5.62            catch {
    5.63              case ERROR(msg) =>
    5.64 -              cat_error(msg, "The error(s) above occurred while examining theory file " +
    5.65 -                quote(node_name) + required_by("\n", initiators))
    5.66 +              cat_error(msg, "The error(s) above occurred while examining theory " +
    5.67 +                quote(name.theory) + required_by(initiators))
    5.68            }
    5.69 -        val thys = header.imports.map(str => (dir1, str))
    5.70 -        require_thys(node_name :: initiators, deps + (node_name -> Exn.Res(header)), thys)
    5.71 +        val imports = header.imports.map(import_name(name.master_dir, _))
    5.72 +        require_thys(name :: initiators, deps + (name -> Exn.Res(header)), imports)
    5.73        }
    5.74 -      catch { case e: Throwable => deps + (node_name -> Exn.Exn(e)) }
    5.75 +      catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
    5.76      }
    5.77    }
    5.78  
    5.79 -  def dependencies(thys: List[(String, String)]): Deps =
    5.80 -    require_thys(Nil, Map.empty, thys)
    5.81 +  def dependencies(names: List[Document.Node.Name]): Deps =
    5.82 +    require_thys(Nil, Map.empty, names)
    5.83  }
     6.1 --- a/src/Pure/Thy/thy_load.scala	Thu Sep 01 11:33:44 2011 +0200
     6.2 +++ b/src/Pure/Thy/thy_load.scala	Thu Sep 01 13:34:45 2011 +0200
     6.3 @@ -11,6 +11,6 @@
     6.4    def register_thy(thy_name: String)
     6.5    def is_loaded(thy_name: String): Boolean
     6.6    def append(master_dir: String, path: Path): String
     6.7 -  def check_thy(node_name: String): Thy_Header
     6.8 +  def check_thy(node_name: Document.Node.Name): Thy_Header
     6.9  }
    6.10  
     7.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Sep 01 11:33:44 2011 +0200
     7.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Sep 01 13:34:45 2011 +0200
     7.3 @@ -27,13 +27,14 @@
     7.4        def length: Int = command.length
     7.5      }
     7.6  
     7.7 -    def parse(syntax: Outer_Syntax, node_name: String, root_name: String, text: CharSequence)
     7.8 +    def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence)
     7.9        : Entry =
    7.10      {
    7.11        /* stack operations */
    7.12  
    7.13        def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
    7.14 -      var stack: List[(Int, String, mutable.ListBuffer[Entry])] = List((0, root_name, buffer()))
    7.15 +      var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
    7.16 +        List((0, "theory " + node_name.theory, buffer()))
    7.17  
    7.18        @tailrec def close(level: Int => Boolean)
    7.19        {
    7.20 @@ -126,7 +127,8 @@
    7.21      }
    7.22    }
    7.23  
    7.24 -  def update_perspective(nodes: Document.Nodes, name: String, text_perspective: Text.Perspective)
    7.25 +  def update_perspective(nodes: Document.Nodes,
    7.26 +      name: Document.Node.Name, text_perspective: Text.Perspective)
    7.27      : (Command.Perspective, Option[Document.Nodes]) =
    7.28    {
    7.29      val node = nodes(name)
    7.30 @@ -137,7 +139,8 @@
    7.31      (perspective, new_nodes)
    7.32    }
    7.33  
    7.34 -  def edit_perspective(previous: Document.Version, name: String, text_perspective: Text.Perspective)
    7.35 +  def edit_perspective(previous: Document.Version,
    7.36 +      name: Document.Node.Name, text_perspective: Text.Perspective)
    7.37      : (Command.Perspective, Document.Version) =
    7.38    {
    7.39      val nodes = previous.nodes
    7.40 @@ -187,7 +190,7 @@
    7.41  
    7.42      /* phase 2: recover command spans */
    7.43  
    7.44 -    @tailrec def recover_spans(node_name: String, commands: Linear_Set[Command])
    7.45 +    @tailrec def recover_spans(node_name: Document.Node.Name, commands: Linear_Set[Command])
    7.46        : Linear_Set[Command] =
    7.47      {
    7.48        commands.iterator.find(cmd => !cmd.is_defined) match {
     8.1 --- a/src/Tools/jEdit/src/document_model.scala	Thu Sep 01 11:33:44 2011 +0200
     8.2 +++ b/src/Tools/jEdit/src/document_model.scala	Thu Sep 01 13:34:45 2011 +0200
     8.3 @@ -45,11 +45,10 @@
     8.4      }
     8.5    }
     8.6  
     8.7 -  def init(session: Session, buffer: Buffer,
     8.8 -    master_dir: String, node_name: String, thy_name: String): Document_Model =
     8.9 +  def init(session: Session, buffer: Buffer, name: Document.Node.Name): Document_Model =
    8.10    {
    8.11      exit(buffer)
    8.12 -    val model = new Document_Model(session, buffer, master_dir, node_name, thy_name)
    8.13 +    val model = new Document_Model(session, buffer, name)
    8.14      buffer.setProperty(key, model)
    8.15      model.activate()
    8.16      model
    8.17 @@ -57,15 +56,14 @@
    8.18  }
    8.19  
    8.20  
    8.21 -class Document_Model(val session: Session, val buffer: Buffer,
    8.22 -  val master_dir: String, val node_name: String, val thy_name: String)
    8.23 +class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name)
    8.24  {
    8.25    /* header */
    8.26  
    8.27    def node_header(): Exn.Result[Thy_Header] =
    8.28    {
    8.29      Swing_Thread.require()
    8.30 -    Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
    8.31 +    Exn.capture { Thy_Header.check(name.theory, buffer.getSegment(0, buffer.getLength)) }
    8.32    }
    8.33  
    8.34  
    8.35 @@ -105,15 +103,14 @@
    8.36          case edits =>
    8.37            pending.clear
    8.38            last_perspective = new_perspective
    8.39 -          session.edit_node(node_name, master_dir, node_header(), new_perspective, edits)
    8.40 +          session.edit_node(name, node_header(), new_perspective, edits)
    8.41        }
    8.42      }
    8.43  
    8.44      def init()
    8.45      {
    8.46        flush()
    8.47 -      session.init_node(node_name, master_dir,
    8.48 -        node_header(), perspective(), Isabelle.buffer_text(buffer))
    8.49 +      session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
    8.50      }
    8.51  
    8.52      private val delay_flush =
    8.53 @@ -145,7 +142,7 @@
    8.54    def snapshot(): Document.Snapshot =
    8.55    {
    8.56      Swing_Thread.require()
    8.57 -    session.snapshot(node_name, pending_edits.snapshot())
    8.58 +    session.snapshot(name, pending_edits.snapshot())
    8.59    }
    8.60  
    8.61  
     9.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Sep 01 11:33:44 2011 +0200
     9.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Sep 01 13:34:45 2011 +0200
     9.3 @@ -449,7 +449,7 @@
     9.4              val visible = visible_range()
     9.5  
     9.6              if (updated ||
     9.7 -                (changed.nodes.contains(model.node_name) &&
     9.8 +                (changed.nodes.contains(model.name) &&
     9.9                   changed.commands.exists(snapshot.node.commands.contains)))
    9.10                overview.repaint()
    9.11  
    10.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Sep 01 11:33:44 2011 +0200
    10.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Thu Sep 01 13:34:45 2011 +0200
    10.3 @@ -77,7 +77,7 @@
    10.4                            case Some((def_node, def_cmd)) =>
    10.5                              def_node.command_start(def_cmd) match {
    10.6                                case Some(def_cmd_start) =>
    10.7 -                                new Internal_Hyperlink(def_cmd.node_name, begin, end, line,
    10.8 +                                new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
    10.9                                    def_cmd_start + def_cmd.decode(def_offset))
   10.10                                case None => null
   10.11                              }
    11.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Sep 01 11:33:44 2011 +0200
    11.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Sep 01 13:34:45 2011 +0200
    11.3 @@ -138,7 +138,7 @@
    11.4        }
    11.5  
    11.6      val text = Isabelle.buffer_text(model.buffer)
    11.7 -    val structure = Structure.parse(syntax, model.node_name, "theory " + model.thy_name, text)
    11.8 +    val structure = Structure.parse(syntax, model.name, text)
    11.9  
   11.10      make_tree(0, structure) foreach (node => data.root.add(node))
   11.11    }
    12.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Thu Sep 01 11:33:44 2011 +0200
    12.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Thu Sep 01 13:34:45 2011 +0200
    12.3 @@ -33,23 +33,23 @@
    12.4  
    12.5    /* file-system operations */
    12.6  
    12.7 -  override def append(master_dir: String, source_path: Path): String =
    12.8 +  override def append(dir: String, source_path: Path): String =
    12.9    {
   12.10      val path = source_path.expand
   12.11      if (path.is_absolute) Isabelle_System.platform_path(path)
   12.12      else {
   12.13 -      val vfs = VFSManager.getVFSForPath(master_dir)
   12.14 +      val vfs = VFSManager.getVFSForPath(dir)
   12.15        if (vfs.isInstanceOf[FileVFS])
   12.16          MiscUtilities.resolveSymlinks(
   12.17 -          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
   12.18 -      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
   12.19 +          vfs.constructPath(dir, Isabelle_System.platform_path(path)))
   12.20 +      else vfs.constructPath(dir, Isabelle_System.standard_path(path))
   12.21      }
   12.22    }
   12.23  
   12.24 -  override def check_thy(node_name: String): Thy_Header =
   12.25 +  override def check_thy(name: Document.Node.Name): Thy_Header =
   12.26    {
   12.27      Swing_Thread.now {
   12.28 -      Isabelle.jedit_buffer(node_name) match {
   12.29 +      Isabelle.jedit_buffer(name.node) match {
   12.30          case Some(buffer) =>
   12.31            Isabelle.buffer_lock(buffer) {
   12.32              val text = new Segment
   12.33 @@ -59,7 +59,7 @@
   12.34          case None => None
   12.35        }
   12.36      } getOrElse {
   12.37 -      val file = new File(node_name)  // FIXME load URL via jEdit VFS (!?)
   12.38 +      val file = new File(name.node)  // FIXME load URL via jEdit VFS (!?)
   12.39        if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
   12.40        Thy_Header.read(file)
   12.41      }
    13.1 --- a/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 11:33:44 2011 +0200
    13.2 +++ b/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 13:34:45 2011 +0200
    13.3 @@ -168,9 +168,6 @@
    13.4  
    13.5    def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    13.6  
    13.7 -  def buffer_path(buffer: Buffer): (String, String) =
    13.8 -    (buffer.getDirectory, buffer_name(buffer))
    13.9 -
   13.10  
   13.11    /* main jEdit components */
   13.12  
   13.13 @@ -216,10 +213,11 @@
   13.14          document_model(buffer) match {
   13.15            case Some(model) => Some(model)
   13.16            case None =>
   13.17 -            val (master_dir, path) = buffer_path(buffer)
   13.18 -            Thy_Header.thy_name(path) match {
   13.19 -              case Some(name) =>
   13.20 -                Some(Document_Model.init(session, buffer, master_dir, path, name))
   13.21 +            val name = buffer_name(buffer)
   13.22 +            Thy_Header.thy_name(name) match {
   13.23 +              case Some(theory) =>
   13.24 +                val node_name = Document.Node.Name(name, buffer.getDirectory, theory)
   13.25 +                Some(Document_Model.init(session, buffer, node_name))
   13.26                case None => None
   13.27              }
   13.28          }
   13.29 @@ -363,8 +361,8 @@
   13.30  
   13.31        val thys =
   13.32          for (buffer <- buffers; model <- Isabelle.document_model(buffer))
   13.33 -          yield (model.master_dir, model.thy_name)
   13.34 -      val files = thy_info.dependencies(thys).toList.map(_._1).filterNot(loaded_buffer _)
   13.35 +          yield model.name
   13.36 +      val files = thy_info.dependencies(thys).toList.map(_._1.node).filterNot(loaded_buffer _)
   13.37  
   13.38        if (!files.isEmpty) {
   13.39          val files_list = new ListView(Library.sort_strings(files))
    14.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Thu Sep 01 11:33:44 2011 +0200
    14.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Thu Sep 01 13:34:45 2011 +0200
    14.3 @@ -75,7 +75,7 @@
    14.4  
    14.5    private var nodes_status: Map[String, String] = Map.empty
    14.6  
    14.7 -  private def handle_changed(changed_nodes: Set[String])
    14.8 +  private def handle_changed(changed_nodes: Set[Document.Node.Name])
    14.9    {
   14.10      Swing_Thread.now {
   14.11        // FIXME correlation to changed_nodes!?
   14.12 @@ -88,7 +88,7 @@
   14.13              name <- changed_nodes
   14.14              node <- version.nodes.get(name)
   14.15              val status = Isar_Document.node_status(state, version, node)
   14.16 -          } nodes_status1 += (name -> status.toString)
   14.17 +          } nodes_status1 += (name.node -> status.toString)
   14.18  
   14.19            if (nodes_status != nodes_status1) {
   14.20              nodes_status = nodes_status1