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 + def import_name(master_dir: String, str: String): Document.Node.Name =
5.27 + {
5.28 + val path = Path.explode(str)
5.29 + val node_name = thy_load.append(master_dir, Thy_Header.thy_path(path))
5.30 + val master_dir1 = thy_load.append(master_dir, path.dir)
5.31 + Document.Node.Name(node_name, master_dir1, path.base.implode)
5.32 + }
5.33
5.34 - private def require_thys(initiators: List[String],
5.35 - deps: Deps, thys: List[(String, String)]): Deps =
5.36 - (deps /: thys)(require_thy(initiators, _, _))
5.37 + type Deps = Map[Document.Node.Name, Document.Node_Header]
5.38
5.39 - private def require_thy(initiators: List[String], deps: Deps, thy: (String, String)): Deps =
5.40 + private def require_thys(initiators: List[Document.Node.Name],
5.41 + deps: Deps, names: List[Document.Node.Name]): Deps =
5.42 + (deps /: names)(require_thy(initiators, _, _))
5.43 +
5.44 + private def require_thy(initiators: List[Document.Node.Name],
5.45 + deps: Deps, name: Document.Node.Name): Deps =
5.46 {
5.47 - val (dir, str) = thy
5.48 - val path = Path.explode(str)
5.49 - val thy_name = path.base.implode
5.50 - val node_name = thy_load.append(dir, Thy_Header.thy_path(path))
5.51 -
5.52 - if (deps.isDefinedAt(node_name) || thy_load.is_loaded(thy_name)) deps
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