# HG changeset patch # User wenzelm # Date 1314876885 -7200 # Node ID a4ff8a7872025a18633cca7fe7a3cbe1b6c58ba0 # Parent 466ea227e00dbf65d9604bfac9ffc7b2b9661da3 more abstract Document.Node.Name; tuned signature; diff -r 466ea227e00d -r a4ff8a787202 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Pure/PIDE/command.scala Thu Sep 01 13:34:45 2011 +0200 @@ -80,9 +80,10 @@ /* dummy commands */ def unparsed(source: String): Command = - new Command(Document.no_id, "", List(Token(Token.Kind.UNPARSED, source))) + new Command(Document.no_id, Document.Node.Name("", "", ""), + List(Token(Token.Kind.UNPARSED, source))) - def span(node_name: String, toks: List[Token]): Command = + def span(node_name: Document.Node.Name, toks: List[Token]): Command = new Command(Document.no_id, node_name, toks) @@ -110,7 +111,7 @@ class Command( val id: Document.Command_ID, - val node_name: String, + val node_name: Document.Node.Name, val span: List[Token]) { /* classification */ diff -r 466ea227e00d -r a4ff8a787202 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Pure/PIDE/document.scala Thu Sep 01 13:34:45 2011 +0200 @@ -31,7 +31,7 @@ /* named nodes -- development graph */ - type Edit[A, B] = (String, Node.Edit[A, B]) + type Edit[A, B] = (Node.Name, Node.Edit[A, B]) type Edit_Text = Edit[Text.Edit, Text.Perspective] type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective] @@ -39,6 +39,16 @@ object Node { + sealed case class Name(node: String, master_dir: String, theory: String) + { + override def hashCode: Int = node.hashCode + override def equals(that: Any): Boolean = + that match { + case other: Name => node == other.node + case _ => false + } + } + sealed abstract class Edit[A, B] { def foreach(f: A => Unit) @@ -149,7 +159,7 @@ val init: Version = Version(no_id, Map().withDefaultValue(Node.empty)) } - type Nodes = Map[String, Node] + type Nodes = Map[Node.Name, Node] sealed case class Version(val id: Version_ID, val nodes: Nodes) @@ -335,10 +345,10 @@ def tip_stable: Boolean = is_stable(history.tip) def tip_version: Version = history.tip.version.get_finished - def last_exec_offset(name: String): Text.Offset = + def last_exec_offset(name: Node.Name): Text.Offset = { val version = tip_version - the_assignment(version).last_execs.get(name) match { + the_assignment(version).last_execs.get(name.node) match { case Some(Some(id)) => val node = version.nodes(name) val cmd = the_command(id).command @@ -371,7 +381,7 @@ // persistent user-view - def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot = + def snapshot(name: Node.Name, pending_edits: List[Text.Edit]): Snapshot = { val stable = recent_stable.get val latest = history.tip diff -r 466ea227e00d -r a4ff8a787202 src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Pure/PIDE/isar_document.scala Thu Sep 01 13:34:45 2011 +0200 @@ -160,14 +160,14 @@ } def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID, - name: String, perspective: Command.Perspective) + name: Document.Node.Name, perspective: Command.Perspective) { val ids = { import XML.Encode._ list(long)(perspective.commands.map(_.id)) } - input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), name, - YXML.string_of_body(ids)) + input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), + name.node, YXML.string_of_body(ids)) } def update(old_id: Document.Version_ID, new_id: Document.Version_ID, @@ -177,7 +177,7 @@ { import XML.Encode._ def id: T[Command] = (cmd => long(cmd.id)) def encode: T[List[Document.Edit_Command]] = - list(pair(string, + list(pair((name => string(name.node)), variant(List( { case Document.Node.Clear() => (Nil, Nil) }, { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, diff -r 466ea227e00d -r a4ff8a787202 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Pure/System/session.scala Thu Sep 01 13:34:45 2011 +0200 @@ -22,7 +22,7 @@ case object Global_Settings case object Perspective case object Assignment - case class Commands_Changed(nodes: Set[String], commands: Set[Command]) + case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command]) sealed abstract class Phase case object Inactive extends Phase @@ -63,7 +63,7 @@ private val (_, command_change_buffer) = Simple_Thread.actor("command_change_buffer", daemon = true) { - var changed_nodes: Set[String] = Set.empty + var changed_nodes: Set[Document.Node.Name] = Set.empty var changed_commands: Set[Command] = Set.empty def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty @@ -134,23 +134,22 @@ private val global_state = new Volatile(Document.State.init) def current_state(): Document.State = global_state() - def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot = + def snapshot(name: Document.Node.Name, pending_edits: List[Text.Edit]): Document.Snapshot = global_state().snapshot(name, pending_edits) /* theory files */ - def header_edit(name: String, master_dir: String, - header: Document.Node_Header): Document.Edit_Text = + def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text = { def norm_import(s: String): String = { val thy_name = Thy_Header.base_name(s) if (thy_load.is_loaded(thy_name)) thy_name - else thy_load.append(master_dir, Thy_Header.thy_path(Path.explode(s))) + else thy_load.append(name.master_dir, Thy_Header.thy_path(Path.explode(s))) } def norm_use(s: String): String = - thy_load.append(master_dir, Path.explode(s)) + thy_load.append(name.master_dir, Path.explode(s)) val header1: Document.Node_Header = header match { @@ -167,12 +166,12 @@ private case class Start(timeout: Time, args: List[String]) private case object Interrupt - private case class Init_Node(name: String, master_dir: String, + private case class Init_Node(name: Document.Node.Name, header: Document.Node_Header, perspective: Text.Perspective, text: String) - private case class Edit_Node(name: String, master_dir: String, + private case class Edit_Node(name: Document.Node.Name, header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit]) private case class Change_Node( - name: String, + name: Document.Node.Name, doc_edits: List[Document.Edit_Command], previous: Document.Version, version: Document.Version) @@ -185,7 +184,7 @@ /* perspective */ - def update_perspective(name: String, text_perspective: Text.Perspective) + def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective) { val previous = global_state().tip_version val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective) @@ -206,7 +205,7 @@ /* incoming edits */ - def handle_edits(name: String, master_dir: String, + def handle_edits(name: Document.Node.Name, header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]]) //{{{ { @@ -215,7 +214,7 @@ prover.get.cancel_execution() - val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit)) + val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit)) val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) } val change = global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2))) @@ -354,20 +353,20 @@ case Interrupt if prover.isDefined => prover.get.interrupt - case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined => + case Init_Node(name, header, perspective, text) if prover.isDefined => // FIXME compare with existing node - handle_edits(name, master_dir, header, + handle_edits(name, header, List(Document.Node.Clear(), Document.Node.Edits(List(Text.Edit.insert(0, text))), Document.Node.Perspective(perspective))) reply(()) - case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined => + case Edit_Node(name, header, perspective, text_edits) if prover.isDefined => if (text_edits.isEmpty && global_state().tip_stable && perspective.range.stop <= global_state().last_exec_offset(name)) update_perspective(name, perspective) else - handle_edits(name, master_dir, header, + handle_edits(name, header, List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective))) reply(()) @@ -396,13 +395,11 @@ def interrupt() { session_actor ! Interrupt } - // FIXME simplify signature - def init_node(name: String, master_dir: String, + def init_node(name: Document.Node.Name, header: Document.Node_Header, perspective: Text.Perspective, text: String) - { session_actor !? Init_Node(name, master_dir, header, perspective, text) } + { session_actor !? Init_Node(name, header, perspective, text) } - // FIXME simplify signature - def edit_node(name: String, master_dir: String, header: Document.Node_Header, - perspective: Text.Perspective, edits: List[Text.Edit]) - { session_actor !? Edit_Node(name, master_dir, header, perspective, edits) } + def edit_node(name: Document.Node.Name, + header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit]) + { session_actor !? Edit_Node(name, header, perspective, edits) } } diff -r 466ea227e00d -r a4ff8a787202 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Pure/Thy/thy_info.scala Thu Sep 01 13:34:45 2011 +0200 @@ -25,51 +25,54 @@ { /* messages */ - private def show_path(names: List[String]): String = - names.map(quote).mkString(" via ") + private def show_path(names: List[Document.Node.Name]): String = + names.map(name => quote(name.theory)).mkString(" via ") - private def cycle_msg(names: List[String]): String = + private def cycle_msg(names: List[Document.Node.Name]): String = "Cyclic dependency of " + show_path(names) - private def required_by(s: String, initiators: List[String]): String = + private def required_by(initiators: List[Document.Node.Name]): String = if (initiators.isEmpty) "" - else s + "(required by " + show_path(initiators.reverse) + ")" + else "\n(required by " + show_path(initiators.reverse) + ")" /* dependencies */ - type Deps = Map[String, Document.Node_Header] - - private def require_thys(initiators: List[String], - deps: Deps, thys: List[(String, String)]): Deps = - (deps /: thys)(require_thy(initiators, _, _)) - - private def require_thy(initiators: List[String], deps: Deps, thy: (String, String)): Deps = + def import_name(master_dir: String, str: String): Document.Node.Name = { - val (dir, str) = thy val path = Path.explode(str) - val thy_name = path.base.implode - val node_name = thy_load.append(dir, Thy_Header.thy_path(path)) + val node_name = thy_load.append(master_dir, Thy_Header.thy_path(path)) + val master_dir1 = thy_load.append(master_dir, path.dir) + Document.Node.Name(node_name, master_dir1, path.base.implode) + } + + type Deps = Map[Document.Node.Name, Document.Node_Header] - if (deps.isDefinedAt(node_name) || thy_load.is_loaded(thy_name)) deps + private def require_thys(initiators: List[Document.Node.Name], + deps: Deps, names: List[Document.Node.Name]): Deps = + (deps /: names)(require_thy(initiators, _, _)) + + private def require_thy(initiators: List[Document.Node.Name], + deps: Deps, name: Document.Node.Name): Deps = + { + if (deps.isDefinedAt(name) || thy_load.is_loaded(name.theory)) deps else { - val dir1 = thy_load.append(dir, path.dir) try { - if (initiators.contains(node_name)) error(cycle_msg(initiators)) + if (initiators.contains(name)) error(cycle_msg(initiators)) val header = - try { thy_load.check_thy(node_name) } + try { thy_load.check_thy(name) } catch { case ERROR(msg) => - cat_error(msg, "The error(s) above occurred while examining theory file " + - quote(node_name) + required_by("\n", initiators)) + cat_error(msg, "The error(s) above occurred while examining theory " + + quote(name.theory) + required_by(initiators)) } - val thys = header.imports.map(str => (dir1, str)) - require_thys(node_name :: initiators, deps + (node_name -> Exn.Res(header)), thys) + val imports = header.imports.map(import_name(name.master_dir, _)) + require_thys(name :: initiators, deps + (name -> Exn.Res(header)), imports) } - catch { case e: Throwable => deps + (node_name -> Exn.Exn(e)) } + catch { case e: Throwable => deps + (name -> Exn.Exn(e)) } } } - def dependencies(thys: List[(String, String)]): Deps = - require_thys(Nil, Map.empty, thys) + def dependencies(names: List[Document.Node.Name]): Deps = + require_thys(Nil, Map.empty, names) } diff -r 466ea227e00d -r a4ff8a787202 src/Pure/Thy/thy_load.scala --- a/src/Pure/Thy/thy_load.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Pure/Thy/thy_load.scala Thu Sep 01 13:34:45 2011 +0200 @@ -11,6 +11,6 @@ def register_thy(thy_name: String) def is_loaded(thy_name: String): Boolean def append(master_dir: String, path: Path): String - def check_thy(node_name: String): Thy_Header + def check_thy(node_name: Document.Node.Name): Thy_Header } diff -r 466ea227e00d -r a4ff8a787202 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Thu Sep 01 13:34:45 2011 +0200 @@ -27,13 +27,14 @@ def length: Int = command.length } - def parse(syntax: Outer_Syntax, node_name: String, root_name: String, text: CharSequence) + def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence) : Entry = { /* stack operations */ def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry] - var stack: List[(Int, String, mutable.ListBuffer[Entry])] = List((0, root_name, buffer())) + var stack: List[(Int, String, mutable.ListBuffer[Entry])] = + List((0, "theory " + node_name.theory, buffer())) @tailrec def close(level: Int => Boolean) { @@ -126,7 +127,8 @@ } } - def update_perspective(nodes: Document.Nodes, name: String, text_perspective: Text.Perspective) + def update_perspective(nodes: Document.Nodes, + name: Document.Node.Name, text_perspective: Text.Perspective) : (Command.Perspective, Option[Document.Nodes]) = { val node = nodes(name) @@ -137,7 +139,8 @@ (perspective, new_nodes) } - def edit_perspective(previous: Document.Version, name: String, text_perspective: Text.Perspective) + def edit_perspective(previous: Document.Version, + name: Document.Node.Name, text_perspective: Text.Perspective) : (Command.Perspective, Document.Version) = { val nodes = previous.nodes @@ -187,7 +190,7 @@ /* phase 2: recover command spans */ - @tailrec def recover_spans(node_name: String, commands: Linear_Set[Command]) + @tailrec def recover_spans(node_name: Document.Node.Name, commands: Linear_Set[Command]) : Linear_Set[Command] = { commands.iterator.find(cmd => !cmd.is_defined) match { diff -r 466ea227e00d -r a4ff8a787202 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Thu Sep 01 13:34:45 2011 +0200 @@ -45,11 +45,10 @@ } } - def init(session: Session, buffer: Buffer, - master_dir: String, node_name: String, thy_name: String): Document_Model = + def init(session: Session, buffer: Buffer, name: Document.Node.Name): Document_Model = { exit(buffer) - val model = new Document_Model(session, buffer, master_dir, node_name, thy_name) + val model = new Document_Model(session, buffer, name) buffer.setProperty(key, model) model.activate() model @@ -57,15 +56,14 @@ } -class Document_Model(val session: Session, val buffer: Buffer, - val master_dir: String, val node_name: String, val thy_name: String) +class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name) { /* header */ def node_header(): Exn.Result[Thy_Header] = { Swing_Thread.require() - Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) } + Exn.capture { Thy_Header.check(name.theory, buffer.getSegment(0, buffer.getLength)) } } @@ -105,15 +103,14 @@ case edits => pending.clear last_perspective = new_perspective - session.edit_node(node_name, master_dir, node_header(), new_perspective, edits) + session.edit_node(name, node_header(), new_perspective, edits) } } def init() { flush() - session.init_node(node_name, master_dir, - node_header(), perspective(), Isabelle.buffer_text(buffer)) + session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer)) } private val delay_flush = @@ -145,7 +142,7 @@ def snapshot(): Document.Snapshot = { Swing_Thread.require() - session.snapshot(node_name, pending_edits.snapshot()) + session.snapshot(name, pending_edits.snapshot()) } diff -r 466ea227e00d -r a4ff8a787202 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Thu Sep 01 13:34:45 2011 +0200 @@ -449,7 +449,7 @@ val visible = visible_range() if (updated || - (changed.nodes.contains(model.node_name) && + (changed.nodes.contains(model.name) && changed.commands.exists(snapshot.node.commands.contains))) overview.repaint() diff -r 466ea227e00d -r a4ff8a787202 src/Tools/jEdit/src/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Thu Sep 01 13:34:45 2011 +0200 @@ -77,7 +77,7 @@ case Some((def_node, def_cmd)) => def_node.command_start(def_cmd) match { case Some(def_cmd_start) => - new Internal_Hyperlink(def_cmd.node_name, begin, end, line, + new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line, def_cmd_start + def_cmd.decode(def_offset)) case None => null } diff -r 466ea227e00d -r a4ff8a787202 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Sep 01 13:34:45 2011 +0200 @@ -138,7 +138,7 @@ } val text = Isabelle.buffer_text(model.buffer) - val structure = Structure.parse(syntax, model.node_name, "theory " + model.thy_name, text) + val structure = Structure.parse(syntax, model.name, text) make_tree(0, structure) foreach (node => data.root.add(node)) } diff -r 466ea227e00d -r a4ff8a787202 src/Tools/jEdit/src/jedit_thy_load.scala --- a/src/Tools/jEdit/src/jedit_thy_load.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala Thu Sep 01 13:34:45 2011 +0200 @@ -33,23 +33,23 @@ /* file-system operations */ - override def append(master_dir: String, source_path: Path): String = + override def append(dir: String, source_path: Path): String = { val path = source_path.expand if (path.is_absolute) Isabelle_System.platform_path(path) else { - val vfs = VFSManager.getVFSForPath(master_dir) + val vfs = VFSManager.getVFSForPath(dir) if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks( - vfs.constructPath(master_dir, Isabelle_System.platform_path(path))) - else vfs.constructPath(master_dir, Isabelle_System.standard_path(path)) + vfs.constructPath(dir, Isabelle_System.platform_path(path))) + else vfs.constructPath(dir, Isabelle_System.standard_path(path)) } } - override def check_thy(node_name: String): Thy_Header = + override def check_thy(name: Document.Node.Name): Thy_Header = { Swing_Thread.now { - Isabelle.jedit_buffer(node_name) match { + Isabelle.jedit_buffer(name.node) match { case Some(buffer) => Isabelle.buffer_lock(buffer) { val text = new Segment @@ -59,7 +59,7 @@ case None => None } } getOrElse { - val file = new File(node_name) // FIXME load URL via jEdit VFS (!?) + val file = new File(name.node) // FIXME load URL via jEdit VFS (!?) if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) Thy_Header.read(file) } diff -r 466ea227e00d -r a4ff8a787202 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Thu Sep 01 13:34:45 2011 +0200 @@ -168,9 +168,6 @@ def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath - def buffer_path(buffer: Buffer): (String, String) = - (buffer.getDirectory, buffer_name(buffer)) - /* main jEdit components */ @@ -216,10 +213,11 @@ document_model(buffer) match { case Some(model) => Some(model) case None => - val (master_dir, path) = buffer_path(buffer) - Thy_Header.thy_name(path) match { - case Some(name) => - Some(Document_Model.init(session, buffer, master_dir, path, name)) + val name = buffer_name(buffer) + Thy_Header.thy_name(name) match { + case Some(theory) => + val node_name = Document.Node.Name(name, buffer.getDirectory, theory) + Some(Document_Model.init(session, buffer, node_name)) case None => None } } @@ -363,8 +361,8 @@ val thys = for (buffer <- buffers; model <- Isabelle.document_model(buffer)) - yield (model.master_dir, model.thy_name) - val files = thy_info.dependencies(thys).toList.map(_._1).filterNot(loaded_buffer _) + yield model.name + val files = thy_info.dependencies(thys).toList.map(_._1.node).filterNot(loaded_buffer _) if (!files.isEmpty) { val files_list = new ListView(Library.sort_strings(files)) diff -r 466ea227e00d -r a4ff8a787202 src/Tools/jEdit/src/session_dockable.scala --- a/src/Tools/jEdit/src/session_dockable.scala Thu Sep 01 11:33:44 2011 +0200 +++ b/src/Tools/jEdit/src/session_dockable.scala Thu Sep 01 13:34:45 2011 +0200 @@ -75,7 +75,7 @@ private var nodes_status: Map[String, String] = Map.empty - private def handle_changed(changed_nodes: Set[String]) + private def handle_changed(changed_nodes: Set[Document.Node.Name]) { Swing_Thread.now { // FIXME correlation to changed_nodes!? @@ -88,7 +88,7 @@ name <- changed_nodes node <- version.nodes.get(name) val status = Isar_Document.node_status(state, version, node) - } nodes_status1 += (name -> status.toString) + } nodes_status1 += (name.node -> status.toString) if (nodes_status != nodes_status1) { nodes_status = nodes_status1