# HG changeset patch # User wenzelm # Date 1376323321 -7200 # Node ID 92d98cc6cec25500a6152fbad18fda0222e05552 # Parent 3e0fe71f3ce14014447502b06600f502d5c391f8# Parent 8e78bd316a535e0a8f4f703242694d79e9c04325 merged diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 12 15:48:57 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Aug 12 18:02:01 2013 +0200 @@ -496,42 +496,43 @@ val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer)) val _ = - Query_Operation.register_parallel sledgehammerN - (fn st => fn [provers_arg, timeout_arg, subgoal_arg, isar_proofs_arg] => - (case try Toplevel.proof_of st of - SOME state => - let - val ctxt = Proof.context_of state + Query_Operation.register sledgehammerN (fn {state = st, args, output_result} => + (case try Toplevel.proof_of st of + SOME state => + let + val [provers_arg, timeout_arg, subgoal_arg, isar_proofs_arg] = args; + val ctxt = Proof.context_of state - val {debug, verbose, overlord, isar_proofs, ...} = get_params Normal ctxt [] - val override_params = - ([("timeout", [timeout_arg]), - ("blocking", ["true"])] @ - (if Option.map Bool.toString isar_proofs <> SOME isar_proofs_arg - then [("isar_proofs", [isar_proofs_arg])] else []) @ - (if debug then [("debug", ["false"])] else []) @ - (if verbose then [("verbose", ["false"])] else []) @ - (if overlord then [("overlord", ["false"])] else [])) - |> map (normalize_raw_param ctxt) + val {debug, verbose, overlord, isar_proofs, ...} = get_params Normal ctxt [] + val override_params = + ([("timeout", [timeout_arg]), + ("blocking", ["true"])] @ + (if Option.map Bool.toString isar_proofs <> SOME isar_proofs_arg + then [("isar_proofs", [isar_proofs_arg])] else []) @ + (if debug then [("debug", ["false"])] else []) @ + (if verbose then [("verbose", ["false"])] else []) @ + (if overlord then [("overlord", ["false"])] else [])) + |> map (normalize_raw_param ctxt) - val i = the_default 1 (Int.fromString subgoal_arg) + val i = the_default 1 (Int.fromString subgoal_arg) - val {provers, ...} = - get_params Normal ctxt - (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) + val {provers, ...} = + get_params Normal ctxt + (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) - fun run prover = - let - val prover_params = ("provers", [prover]) :: override_params - val sledgehammer_params = get_params Normal ctxt prover_params - val minimize = minimize_command prover_params i - val (_, (_, state')) = - state - |> Proof.map_context (Config.put sledgehammer_result_request true) - |> run_sledgehammer sledgehammer_params Try i no_fact_override minimize - in Config.get (Proof.context_of state') sledgehammer_result end + fun run prover = + let + val prover_params = ("provers", [prover]) :: override_params + val sledgehammer_params = get_params Normal ctxt prover_params + val minimize = minimize_command prover_params i + val (_, (_, state')) = + state + |> Proof.map_context (Config.put sledgehammer_result_request true) + |> run_sledgehammer sledgehammer_params Try i no_fact_override minimize + in output_result (Config.get (Proof.context_of state') sledgehammer_result) end - in map (fn prover => fn () => run prover) provers end - | NONE => error "Unknown proof context")); + val _ = Par_Exn.release_all (Par_List.map (Exn.interruptible_capture run) provers); + in () end + | NONE => error "Unknown proof context")); end; diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/HOL/Unix/Unix.thy --- a/src/HOL/Unix/Unix.thy Mon Aug 12 15:48:57 2013 +0200 +++ b/src/HOL/Unix/Unix.thy Mon Aug 12 18:02:01 2013 +0200 @@ -843,8 +843,6 @@ neither owned nor writable by @{term user\<^isub>1}. *} - - definition "invariant root path = (\att dir. diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Pure/General/multi_map.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/multi_map.scala Mon Aug 12 18:02:01 2013 +0200 @@ -0,0 +1,68 @@ +/* Title: Pure/General/multi_map.scala + Module: PIDE + +Maps with multiple entries per key. +*/ + +package isabelle + +import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom} + + +object Multi_Map extends ImmutableMapFactory[Multi_Map] +{ + private val empty_val: Multi_Map[Any, Nothing] = new Multi_Map[Any, Nothing](Map.empty) + override def empty[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]] + + implicit def canBuildFrom[A, B]: CanBuildFrom[Coll, (A, B), Multi_Map[A, B]] = + new MapCanBuildFrom[A, B] +} + + +final class Multi_Map[A, +B] private(rep: Map[A, List[B]]) + extends scala.collection.immutable.Map[A, B] + with scala.collection.immutable.MapLike[A, B, Multi_Map[A, B]] +{ + /* Multi_Map operations */ + + def get_list(a: A): List[B] = rep.getOrElse(a, Nil) + + def insert[B1 >: B](a: A, b: B1): Multi_Map[A, B1] = + { + val bs = get_list(a) + if (bs.contains(b)) this + else new Multi_Map(rep + (a -> (b :: bs))) + } + + def remove[B1 >: B](a: A, b: B1): Multi_Map[A, B1] = + { + val bs = get_list(a) + if (bs.contains(b)) { + bs.filterNot(_ == b) match { + case Nil => new Multi_Map(rep - a) + case bs1 => new Multi_Map(rep + (a -> bs1)) + } + } + else this + } + + + /* Map operations */ + + override def stringPrefix = "Multi_Map" + + override def empty = Multi_Map.empty + override def isEmpty: Boolean = rep.isEmpty + + override def keySet: Set[A] = rep.keySet + + override def iterator: Iterator[(A, B)] = + for ((a, bs) <- rep.iterator; b <- bs.iterator) yield (a, b) + + def get(a: A): Option[B] = get_list(a).headOption + + def + [B1 >: B](p: (A, B1)): Multi_Map[A, B1] = insert(p._1, p._2) + + def - (a: A): Multi_Map[A, B] = + if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this +} diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Pure/PIDE/document.scala Mon Aug 12 18:02:01 2013 +0200 @@ -15,6 +15,32 @@ { /** document structure **/ + /* overlays -- print functions with arguments */ + + object Overlays + { + val empty = new Overlays(Map.empty) + } + + final class Overlays private(rep: Map[Node.Name, Node.Overlays]) + { + def apply(name: Document.Node.Name): Node.Overlays = + rep.getOrElse(name, Node.Overlays.empty) + + private def update(name: Node.Name, f: Node.Overlays => Node.Overlays): Overlays = + { + val node_overlays = f(apply(name)) + new Overlays(if (node_overlays.is_empty) rep - name else rep + (name -> node_overlays)) + } + + def insert(command: Command, fn: String, args: List[String]): Overlays = + update(command.node_name, _.insert(command, fn, args)) + + def remove(command: Command, fn: String, args: List[String]): Overlays = + update(command.node_name, _.remove(command, fn, args)) + } + + /* individual nodes */ type Edit[A, B] = (Node.Name, Node.Edit[A, B]) @@ -60,45 +86,22 @@ } - /* overlays -- print functions with arguments */ - - type Overlay = (Command, (String, List[String])) + /* node overlays */ object Overlays { - val empty = new Overlays(Map.empty) + val empty = new Overlays(Multi_Map.empty) } - final class Overlays private(rep: Map[Command, List[(String, List[String])]]) + final class Overlays private(rep: Multi_Map[Command, (String, List[String])]) { def commands: Set[Command] = rep.keySet def is_empty: Boolean = rep.isEmpty - - def insert(cmd: Command, over: (String, List[String])): Overlays = - { - val overs = rep.getOrElse(cmd, Nil) - if (overs.contains(over)) this - else new Overlays(rep + (cmd -> (over :: overs))) - } - - def remove(cmd: Command, over: (String, List[String])): Overlays = - rep.get(cmd) match { - case Some(overs) => - if (overs.contains(over)) { - overs.filterNot(_ == over) match { - case Nil => new Overlays(rep - cmd) - case overs1 => new Overlays(rep + (cmd -> overs1)) - } - } - else this - case None => this - } - - def dest: List[Overlay] = - (for { - (cmd, overs) <- rep.iterator - over <- overs - } yield (cmd, over)).toList + def dest: List[(Command, (String, List[String]))] = rep.iterator.toList + def insert(cmd: Command, fn: String, args: List[String]): Overlays = + new Overlays(rep.insert(cmd, (fn, args))) + def remove(cmd: Command, fn: String, args: List[String]): Overlays = + new Overlays(rep.remove(cmd, (fn, args))) } @@ -205,12 +208,6 @@ def command_range(range: Text.Range): Iterator[(Command, Text.Offset)] = command_range(range.start) takeWhile { case (_, start) => start < range.stop } - def command_at(i: Text.Offset): Option[(Command, Text.Offset)] = - { - val range = command_range(i) - if (range.hasNext) Some(range.next) else None - } - def command_start(cmd: Command): Option[Text.Offset] = Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2) } @@ -324,17 +321,23 @@ /** global state -- document structure, execution process, editing history **/ + object Snapshot + { + val init = State.init.snapshot() + } + abstract class Snapshot { val state: State val version: Version - val node_name: Node.Name - val node: Node val is_outdated: Boolean def convert(i: Text.Offset): Text.Offset def revert(i: Text.Offset): Text.Offset def convert(range: Text.Range): Text.Range def revert(range: Text.Range): Text.Range + + val node_name: Node.Name + val node: Node def eq_content(other: Snapshot): Boolean def cumulate_markup[A]( range: Text.Range, @@ -555,10 +558,10 @@ new Snapshot { + /* global information */ + val state = State.this val version = stable.version.get_finished - val node_name = name - val node = version.nodes(name) val is_outdated = !(pending_edits.isEmpty && latest == stable) def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i)) @@ -566,6 +569,12 @@ def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r)) def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r)) + + /* local node content */ + + val node_name = name + val node = version.nodes(name) + def eq_content(other: Snapshot): Boolean = !is_outdated && !other.is_outdated && node.commands.size == other.node.commands.size && diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Pure/PIDE/editor.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/editor.scala Mon Aug 12 18:02:01 2013 +0200 @@ -0,0 +1,29 @@ +/* Title: Pure/PIDE/editor.scala + Author: Makarius + +General editor operations. +*/ + +package isabelle + + +abstract class Editor[Context] +{ + def session: Session + def flush(): Unit + def current_context: Context + def current_node(context: Context): Option[Document.Node.Name] + def current_node_snapshot(context: Context): Option[Document.Snapshot] + def node_snapshot(name: Document.Node.Name): Document.Snapshot + def current_command(context: Context, snapshot: Document.Snapshot): Option[(Command, Text.Offset)] + + def node_overlays(name: Document.Node.Name): Document.Node.Overlays + def insert_overlay(command: Command, fn: String, args: List[String]): Unit + def remove_overlay(command: Command, fn: String, args: List[String]): Unit + + abstract class Hyperlink { def follow(context: Context): Unit } + def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink + def hyperlink_command( + snapshot: Document.Snapshot, command: Command, offset: Text.Offset = 0): Option[Hyperlink] +} + diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Pure/PIDE/query_operation.ML --- a/src/Pure/PIDE/query_operation.ML Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Pure/PIDE/query_operation.ML Mon Aug 12 18:02:01 2013 +0200 @@ -7,14 +7,14 @@ signature QUERY_OPERATION = sig - val register_parallel: string -> (Toplevel.state -> string list -> (unit -> string) list) -> unit - val register: string -> (Toplevel.state -> string list -> string) -> unit + val register: string -> + ({state: Toplevel.state, args: string list, output_result: string -> unit} -> unit) -> unit end; structure Query_Operation: QUERY_OPERATION = struct -fun register_parallel name f = +fun register name f = Command.print_function name (fn {args = instance :: args, ...} => SOME {delay = NONE, pri = 0, persistent = false, strict = false, @@ -22,23 +22,19 @@ let fun result s = Output.result [(Markup.instanceN, instance)] s; fun status m = result (Markup.markup_only m); + fun output_result s = result (Markup.markup (Markup.writelnN, []) s); fun toplevel_error exn = result (Markup.markup (Markup.errorN, []) (ML_Compiler.exn_message exn)); val _ = status Markup.running; - val outputs = - Multithreading.interruptible (fn () => f state args) () - handle exn (*sic!*) => (toplevel_error exn; []); - val _ = outputs |> Par_List.map (fn out => - (case Exn.capture (restore_attributes out) () (*sic!*) of - Exn.Res s => result (Markup.markup (Markup.writelnN, []) s) - | Exn.Exn exn => toplevel_error exn)); + fun run () = f {state = state, args = args, output_result = output_result}; + val _ = + (case Exn.capture (*sic!*) (restore_attributes run) () of + Exn.Res () => () + | Exn.Exn exn => toplevel_error exn); val _ = status Markup.finished; in () end)} | _ => NONE); -fun register name f = - register_parallel name (fn st => fn args => [fn () => f st args]); - end; diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Pure/PIDE/query_operation.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/query_operation.scala Mon Aug 12 18:02:01 2013 +0200 @@ -0,0 +1,203 @@ +/* Title: Pure/PIDE/query_operation.scala + Author: Makarius + +One-shot query operations via asynchronous print functions and temporary +document overlays. +*/ + +package isabelle + + +import scala.actors.Actor._ + + +object Query_Operation +{ + object Status extends Enumeration + { + val WAITING = Value("waiting") + val RUNNING = Value("running") + val FINISHED = Value("finished") + } +} + +class Query_Operation[Editor_Context]( + editor: Editor[Editor_Context], + editor_context: Editor_Context, + operation_name: String, + consume_status: Query_Operation.Status.Value => Unit, + consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit) +{ + private val instance = Document_ID.make().toString + + + /* implicit state -- owned by Swing thread */ + + private var current_location: Option[Command] = None + private var current_query: List[String] = Nil + private var current_update_pending = false + private var current_output: List[XML.Tree] = Nil + private var current_status = Query_Operation.Status.FINISHED + private var current_exec_id = Document_ID.none + + private def reset_state() + { + current_location = None + current_query = Nil + current_update_pending = false + current_output = Nil + current_status = Query_Operation.Status.FINISHED + current_exec_id = Document_ID.none + } + + private def remove_overlay() + { + current_location.foreach(command => + editor.remove_overlay(command, operation_name, instance :: current_query)) + } + + + /* content update */ + + private def content_update() + { + Swing_Thread.require() + + + /* snapshot */ + + val (snapshot, state, removed) = + current_location match { + case Some(cmd) => + val snapshot = editor.node_snapshot(cmd.node_name) + val state = snapshot.state.command_state(snapshot.version, cmd) + val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd) + (snapshot, state, removed) + case None => + (Document.Snapshot.init, Command.empty.init_state, true) + } + + val results = + (for { + (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries + if props.contains((Markup.INSTANCE, instance)) + } yield elem).toList + + + /* output */ + + val new_output = + for { + XML.Elem(_, List(XML.Elem(markup, body))) <- results + if Markup.messages.contains(markup.name) + } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body) + + + /* status */ + + def get_status(name: String, status: Query_Operation.Status.Value) + : Option[Query_Operation.Status.Value] = + results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status }) + + val new_status = + if (removed) Query_Operation.Status.FINISHED + else + get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse + get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse + Query_Operation.Status.WAITING + + if (new_status == Query_Operation.Status.RUNNING) + results.collectFirst( + { + case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem)) + if elem.name == Markup.RUNNING => id + }).foreach(id => current_exec_id = id) + + + /* state update */ + + if (current_output != new_output || current_status != new_status) { + if (snapshot.is_outdated) + current_update_pending = true + else { + current_update_pending = false + if (current_output != new_output && !removed) { + current_output = new_output + consume_output(snapshot, state.results, new_output) + } + if (current_status != new_status) { + current_status = new_status + consume_status(new_status) + if (new_status == Query_Operation.Status.FINISHED) { + remove_overlay() + editor.flush() + } + } + } + } + } + + + /* query operations */ + + def cancel_query(): Unit = + Swing_Thread.require { editor.session.cancel_exec(current_exec_id) } + + def apply_query(query: List[String]) + { + Swing_Thread.require() + + editor.current_node_snapshot(editor_context) match { + case Some(snapshot) => + remove_overlay() + reset_state() + consume_output(Document.Snapshot.init, Command.Results.empty, Nil) + editor.current_command(editor_context, snapshot) match { + case Some((command, _)) => + current_location = Some(command) + current_query = query + current_status = Query_Operation.Status.WAITING + editor.insert_overlay(command, operation_name, instance :: query) + case None => + } + consume_status(current_status) + editor.flush() + case None => + } + } + + def locate_query() + { + Swing_Thread.require() + + for { + command <- current_location + snapshot = editor.node_snapshot(command.node_name) + link <- editor.hyperlink_command(snapshot, command) + } link.follow(editor_context) + } + + + /* main actor */ + + private val main_actor = actor { + loop { + react { + case changed: Session.Commands_Changed => + current_location match { + case Some(command) + if current_update_pending || + (current_status != Query_Operation.Status.FINISHED && + changed.commands.contains(command)) => + Swing_Thread.later { content_update() } + case _ => + } + case bad => + java.lang.System.err.println("Query_Operation: ignoring bad message " + bad) + } + } + } + + def activate() { editor.session.commands_changed += main_actor } + def deactivate() { editor.session.commands_changed -= main_actor } +} diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Pure/Tools/find_theorems.ML Mon Aug 12 18:02:01 2013 +0200 @@ -575,17 +575,17 @@ (** PIDE query operation **) val _ = - Query_Operation.register "find_theorems" - (fn st => fn [limit_arg, allow_dups_arg, context_arg, query_arg] => - if can Toplevel.context_of st then - let - val state = - if context_arg = "" then proof_state st - else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg)); - val opt_limit = Int.fromString limit_arg; - val rem_dups = allow_dups_arg = "false"; - val criteria = read_query Position.none query_arg; - in Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria) end - else error "Unknown context"); + Query_Operation.register "find_theorems" (fn {state = st, args, output_result} => + if can Toplevel.context_of st then + let + val [limit_arg, allow_dups_arg, context_arg, query_arg] = args; + val state = + if context_arg = "" then proof_state st + else Proof.init (Proof_Context.init_global (Thy_Info.get_theory context_arg)); + val opt_limit = Int.fromString limit_arg; + val rem_dups = allow_dups_arg = "false"; + val criteria = read_query Position.none query_arg; + in output_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end + else error "Unknown context"); end; diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Pure/build-jars --- a/src/Pure/build-jars Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Pure/build-jars Mon Aug 12 18:02:01 2013 +0200 @@ -18,6 +18,7 @@ General/graph.scala General/graphics_file.scala General/linear_set.scala + General/multi_map.scala General/path.scala General/position.scala General/pretty.scala @@ -35,9 +36,11 @@ PIDE/command.scala PIDE/document.scala PIDE/document_id.scala + PIDE/editor.scala PIDE/markup.scala PIDE/markup_tree.scala PIDE/protocol.scala + PIDE/query_operation.scala PIDE/text.scala PIDE/xml.scala PIDE/yxml.scala diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Mon Aug 12 18:02:01 2013 +0200 @@ -17,13 +17,13 @@ "src/fold_handling.scala" "src/graphview_dockable.scala" "src/html_panel.scala" - "src/hyperlink.scala" "src/info_dockable.scala" "src/isabelle.scala" "src/isabelle_encoding.scala" "src/isabelle_logic.scala" "src/isabelle_options.scala" "src/isabelle_sidekick.scala" + "src/jedit_editor.scala" "src/jedit_lib.scala" "src/jedit_main.scala" "src/jedit_options.scala" @@ -36,7 +36,6 @@ "src/pretty_tooltip.scala" "src/process_indicator.scala" "src/protocol_dockable.scala" - "src/query_operation.scala" "src/raw_output_dockable.scala" "src/readme_dockable.scala" "src/rendering.scala" diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Mon Aug 12 18:02:01 2013 +0200 @@ -46,11 +46,11 @@ } } - def init(session: Session, buffer: Buffer, name: Document.Node.Name): Document_Model = + def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model = { Swing_Thread.require() apply(buffer).map(_.deactivate) - val model = new Document_Model(session, buffer, name) + val model = new Document_Model(session, buffer, node_name) buffer.setProperty(key, model) model.activate() buffer.propertiesChanged @@ -59,7 +59,7 @@ } -class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name) +class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name) { /* header */ @@ -68,7 +68,7 @@ Swing_Thread.require() JEdit_Lib.buffer_lock(buffer) { Exn.capture { - PIDE.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength)) + PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength)) } match { case Exn.Res(header) => header case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn)) @@ -77,17 +77,6 @@ } - /* overlays */ - - private var overlays = Document.Node.Overlays.empty - - def insert_overlay(command: Command, name: String, args: List[String]): Unit = - Swing_Thread.require { overlays = overlays.insert(command, (name, args)) } - - def remove_overlay(command: Command, name: String, args: List[String]): Unit = - Swing_Thread.require { overlays = overlays.remove(command, (name, args)) } - - /* perspective */ // owned by Swing thread @@ -99,7 +88,7 @@ if (_node_required != b) { _node_required = b PIDE.options_changed() - PIDE.flush_buffers() + PIDE.editor.flush() } } @@ -115,7 +104,7 @@ for { doc_view <- PIDE.document_views(buffer) range <- doc_view.perspective().ranges - } yield range), overlays) + } yield range), PIDE.editor.node_overlays(node_name)) } else empty_perspective } @@ -131,10 +120,10 @@ val text = JEdit_Lib.buffer_text(buffer) val perspective = node_perspective() - List(session.header_edit(name, header), - name -> Document.Node.Clear(), - name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), - name -> perspective) + List(session.header_edit(node_name, header), + node_name -> Document.Node.Clear(), + node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))), + node_name -> perspective) } def node_edits(perspective: Document.Node.Perspective_Text, text_edits: List[Text.Edit]) @@ -144,9 +133,9 @@ val header = node_header() - List(session.header_edit(name, header), - name -> Document.Node.Edits(text_edits), - name -> perspective) + List(session.header_edit(node_name, header), + node_name -> Document.Node.Edits(text_edits), + node_name -> perspective) } @@ -208,7 +197,7 @@ def snapshot(): Document.Snapshot = { Swing_Thread.require() - session.snapshot(name, pending_edits.snapshot()) + session.snapshot(node_name, pending_edits.snapshot()) } diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Mon Aug 12 18:02:01 2013 +0200 @@ -197,7 +197,7 @@ val snapshot = model.snapshot() if (changed.assignment || - (changed.nodes.contains(model.name) && + (changed.nodes.contains(model.node_name) && changed.commands.exists(snapshot.node.commands.contains))) Swing_Thread.later { overview.delay_repaint.invoke() } diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/documentation_dockable.scala --- a/src/Tools/jEdit/src/documentation_dockable.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/documentation_dockable.scala Mon Aug 12 18:02:01 2013 +0200 @@ -66,7 +66,7 @@ "Documentation error", GUI.scrollable_text(Exn.message(exn))) }) case Text_File(_, path) => - Hyperlink(Isabelle_System.platform_path(path)).follow(view) + PIDE.editor.goto(view, Isabelle_System.platform_path(path)) case _ => } case _ => diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/find_dockable.scala --- a/src/Tools/jEdit/src/find_dockable.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/find_dockable.scala Mon Aug 12 18:02:01 2013 +0200 @@ -46,7 +46,7 @@ } private val find_theorems = - Query_Operation(view, "find_theorems", consume_status _, + new Query_Operation(PIDE.editor, view, "find_theorems", consume_status _, (snapshot, results, body) => pretty_text_area.update(snapshot, results, Pretty.separate(body))) diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/graphview_dockable.scala --- a/src/Tools/jEdit/src/graphview_dockable.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/graphview_dockable.scala Mon Aug 12 18:02:01 2013 +0200 @@ -22,7 +22,7 @@ { /* implicit arguments -- owned by Swing thread */ - private var implicit_snapshot = Document.State.init.snapshot() + private var implicit_snapshot = Document.Snapshot.init private val no_graph: Exn.Result[graphview.Model.Graph] = Exn.Exn(ERROR("No graph")) private var implicit_graph = no_graph @@ -36,7 +36,7 @@ } private def reset_implicit(): Unit = - set_implicit(Document.State.init.snapshot(), no_graph) + set_implicit(Document.Snapshot.init, no_graph) def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph]) { diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/hyperlink.scala --- a/src/Tools/jEdit/src/hyperlink.scala Mon Aug 12 15:48:57 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,58 +0,0 @@ -/* Title: Tools/jEdit/src/hyperlink.scala - Author: Fabian Immler, TU Munich - Author: Makarius - -Hyperlinks within jEdit buffers for PIDE proof documents. -*/ - -package isabelle.jedit - - -import isabelle._ - -import org.gjt.sp.jedit.{View, jEdit} -import org.gjt.sp.jedit.textarea.JEditTextArea - - -object Hyperlink -{ - def apply(jedit_file: String, line: Int = 0, column: Int = 0): Hyperlink = - File_Link(jedit_file, line, column) -} - -abstract class Hyperlink -{ - def follow(view: View): Unit -} - -private case class File_Link(jedit_file: String, line: Int, column: Int) extends Hyperlink -{ - override def follow(view: View) - { - Swing_Thread.require() - - JEdit_Lib.jedit_buffer(jedit_file) match { - case Some(buffer) => - view.goToBuffer(buffer) - val text_area = view.getTextArea - - try { - val line_start = text_area.getBuffer.getLineStartOffset(line - 1) - text_area.moveCaretPosition(line_start) - if (column > 0) text_area.moveCaretPosition(line_start + column - 1) - } - catch { - case _: ArrayIndexOutOfBoundsException => - case _: IllegalArgumentException => - } - - case None => - val args = - if (line <= 0) Array(jedit_file) - else if (column <= 0) Array(jedit_file, "+line:" + line.toInt) - else Array(jedit_file, "+line:" + line.toInt + "," + column.toInt) - jEdit.openFiles(view, null, args) - } - } -} - diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/info_dockable.scala --- a/src/Tools/jEdit/src/info_dockable.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/info_dockable.scala Mon Aug 12 18:02:01 2013 +0200 @@ -25,7 +25,7 @@ { /* implicit arguments -- owned by Swing thread */ - private var implicit_snapshot = Document.State.init.snapshot() + private var implicit_snapshot = Document.Snapshot.init private var implicit_results = Command.Results.empty private var implicit_info: XML.Body = Nil @@ -39,7 +39,7 @@ } private def reset_implicit(): Unit = - set_implicit(Document.State.init.snapshot(), Command.Results.empty, Nil) + set_implicit(Document.Snapshot.init, Command.Results.empty, Nil) def apply(view: View, snapshot: Document.Snapshot, results: Command.Results, info: XML.Body) { diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Mon Aug 12 18:02:01 2013 +0200 @@ -70,7 +70,7 @@ if (continuous_checking != b) { PIDE.options.bool(CONTINUOUS_CHECKING) = b PIDE.options_changed() - PIDE.flush_buffers() + PIDE.editor.flush() } } diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/jedit_editor.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Aug 12 18:02:01 2013 +0200 @@ -0,0 +1,149 @@ +/* Title: Tools/jEdit/src/jedit_editor.scala + Author: Makarius + +PIDE editor operations for jEdit. +*/ + +package isabelle.jedit + + +import isabelle._ + + +import org.gjt.sp.jedit.{jEdit, View} + + +class JEdit_Editor extends Editor[View] +{ + /* session */ + + override def session: Session = PIDE.session + + override def flush() + { + Swing_Thread.require() + + session.update( + (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) { + case (edits, buffer) => + JEdit_Lib.buffer_lock(buffer) { + PIDE.document_model(buffer) match { + case Some(model) => model.flushed_edits() ::: edits + case None => edits + } + } + } + ) + } + + + /* current situation */ + + override def current_context: View = + Swing_Thread.require { jEdit.getActiveView() } + + override def current_node(view: View): Option[Document.Node.Name] = + Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) } + + override def current_node_snapshot(view: View): Option[Document.Snapshot] = + Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) } + + override def node_snapshot(name: Document.Node.Name): Document.Snapshot = + { + Swing_Thread.require() + + JEdit_Lib.jedit_buffer(name.node) match { + case Some(buffer) => + PIDE.document_model(buffer) match { + case Some(model) => model.snapshot + case None => session.snapshot(name) + } + case None => session.snapshot(name) + } + } + + override def current_command(view: View, snapshot: Document.Snapshot) + : Option[(Command, Text.Offset)] = + { + Swing_Thread.require() + + if (snapshot.is_outdated) None + else { + val text_area = view.getTextArea + PIDE.document_view(text_area) match { + case Some(doc_view) => + val node = snapshot.version.nodes(doc_view.model.node_name) + val caret_commands = node.command_range(text_area.getCaretPosition) + if (caret_commands.hasNext) Some(caret_commands.next) else None + case None => None + } + } + } + + + /* overlays */ + + private var overlays = Document.Overlays.empty + + override def node_overlays(name: Document.Node.Name): Document.Node.Overlays = + synchronized { overlays(name) } + + override def insert_overlay(command: Command, fn: String, args: List[String]): Unit = + synchronized { overlays = overlays.insert(command, fn, args) } + + override def remove_overlay(command: Command, fn: String, args: List[String]): Unit = + synchronized { overlays = overlays.remove(command, fn, args) } + + + /* hyperlinks */ + + def goto(view: View, file_name: String, line: Int = 0, column: Int = 0) + { + Swing_Thread.require() + + JEdit_Lib.jedit_buffer(file_name) match { + case Some(buffer) => + view.goToBuffer(buffer) + val text_area = view.getTextArea + + try { + val line_start = text_area.getBuffer.getLineStartOffset(line - 1) + text_area.moveCaretPosition(line_start) + if (column > 0) text_area.moveCaretPosition(line_start + column - 1) + } + catch { + case _: ArrayIndexOutOfBoundsException => + case _: IllegalArgumentException => + } + + case None => + val args = + if (line <= 0) Array(file_name) + else if (column <= 0) Array(file_name, "+line:" + line.toInt) + else Array(file_name, "+line:" + line.toInt + "," + column.toInt) + jEdit.openFiles(view, null, args) + } + } + + override def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink = + new Hyperlink { def follow(view: View) = goto(view, file_name, line, column) } + + override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0) + : Option[Hyperlink] = + { + if (snapshot.is_outdated) None + else { + snapshot.state.find_command(snapshot.version, command.id) match { + case None => None + case Some((node, _)) => + val file_name = command.node_name.node + val sources = + node.commands.iterator.takeWhile(_ != command).map(_.source) ++ + (if (offset == 0) Iterator.empty + else Iterator.single(command.source(Text.Range(0, command.decode(offset))))) + val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column) + Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } }) + } + } + } +} diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Mon Aug 12 18:02:01 2013 +0200 @@ -30,7 +30,7 @@ private var zoom_factor = 100 private var do_update = true - private var current_snapshot = Document.State.init.snapshot() + private var current_snapshot = Document.Snapshot.init private var current_state = Command.empty.init_state private var current_output: List[XML.Tree] = Nil @@ -54,15 +54,14 @@ Swing_Thread.require() val (new_snapshot, new_state) = - Document_View(view.getTextArea) match { - case Some(doc_view) => - val snapshot = doc_view.model.snapshot() + PIDE.editor.current_node_snapshot(view) match { + case Some(snapshot) => if (follow && !snapshot.is_outdated) { - snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { - case Some(cmd) => + PIDE.editor.current_command(view, snapshot) match { + case Some((cmd, _)) => (snapshot, snapshot.state.command_state(snapshot.version, cmd)) case None => - (Document.State.init.snapshot(), Command.empty.init_state) + (Document.Snapshot.init, Command.empty.init_state) } } else (current_snapshot, current_state) diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Mon Aug 12 18:02:01 2013 +0200 @@ -47,23 +47,11 @@ else Some(current_session.recent_syntax) } + lazy val editor = new JEdit_Editor + /* document model and view */ - def document_snapshot(name: Document.Node.Name): Document.Snapshot = - { - Swing_Thread.require() - - JEdit_Lib.jedit_buffer(name.node) match { - case Some(buffer) => - document_model(buffer) match { - case Some(model) => model.snapshot - case None => session.snapshot(name) - } - case None => session.snapshot(name) - } - } - def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer) def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area) @@ -95,7 +83,7 @@ thy_load.buffer_node_name(buffer) match { case Some(node_name) => document_model(buffer) match { - case Some(model) if model.name == node_name => (Nil, Some(model)) + case Some(model) if model.node_name == node_name => (Nil, Some(model)) case _ => val model = Document_Model.init(session, buffer, node_name) (model.init_edits(), Some(model)) @@ -131,23 +119,6 @@ Document_View.exit(text_area) } } - - def flush_buffers() - { - Swing_Thread.require() - - session.update( - (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) { - case (edits, buffer) => - JEdit_Lib.buffer_lock(buffer) { - document_model(buffer) match { - case Some(model) => model.flushed_edits() ::: edits - case None => edits - } - } - } - ) - } } @@ -173,7 +144,7 @@ val thys = for (buffer <- buffers; model <- PIDE.document_model(buffer)) - yield model.name + yield model.node_name val thy_info = new Thy_Info(PIDE.thy_load) // FIXME avoid I/O in Swing thread!?! diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Mon Aug 12 18:02:01 2013 +0200 @@ -64,7 +64,7 @@ private var current_font_family = "Dialog" private var current_font_size: Int = 12 private var current_body: XML.Body = Nil - private var current_base_snapshot = Document.State.init.snapshot() + private var current_base_snapshot = Document.Snapshot.init private var current_base_results = Command.Results.empty private var current_rendering: Rendering = Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2 diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/query_operation.scala --- a/src/Tools/jEdit/src/query_operation.scala Mon Aug 12 15:48:57 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,226 +0,0 @@ -/* Title: Tools/jEdit/src/query_operation.scala - Author: Makarius - -One-shot query operations via asynchronous print functions and temporary -document overlays. -*/ - -package isabelle.jedit - - -import isabelle._ - -import scala.actors.Actor._ - -import org.gjt.sp.jedit.View - - -object Query_Operation -{ - object Status extends Enumeration - { - val WAITING = Value("waiting") - val RUNNING = Value("running") - val FINISHED = Value("finished") - } - - def apply( - view: View, - operation_name: String, - consume_status: Status.Value => Unit, - consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit) = - new Query_Operation(view, operation_name, consume_status, consume_output) -} - -final class Query_Operation private( - view: View, - operation_name: String, - consume_status: Query_Operation.Status.Value => Unit, - consume_output: (Document.Snapshot, Command.Results, XML.Body) => Unit) -{ - private val instance = Document_ID.make().toString - - - /* implicit state -- owned by Swing thread */ - - private var current_location: Option[Command] = None - private var current_query: List[String] = Nil - private var current_update_pending = false - private var current_output: List[XML.Tree] = Nil - private var current_status = Query_Operation.Status.FINISHED - private var current_exec_id = Document_ID.none - - private def reset_state() - { - current_location = None - current_query = Nil - current_update_pending = false - current_output = Nil - current_status = Query_Operation.Status.FINISHED - current_exec_id = Document_ID.none - } - - private def remove_overlay() - { - Swing_Thread.require() - - for { - command <- current_location - buffer <- JEdit_Lib.jedit_buffer(command.node_name.node) - model <- PIDE.document_model(buffer) - } model.remove_overlay(command, operation_name, instance :: current_query) - } - - - /* content update */ - - private def content_update() - { - Swing_Thread.require() - - - /* snapshot */ - - val (snapshot, state, removed) = - current_location match { - case Some(cmd) => - val snapshot = PIDE.document_snapshot(cmd.node_name) - val state = snapshot.state.command_state(snapshot.version, cmd) - val removed = !snapshot.version.nodes(cmd.node_name).commands.contains(cmd) - (snapshot, state, removed) - case None => - (Document.State.init.snapshot(), Command.empty.init_state, true) - } - - val results = - (for { - (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- state.results.entries - if props.contains((Markup.INSTANCE, instance)) - } yield elem).toList - - - /* output */ - - val new_output = - for { - XML.Elem(_, List(XML.Elem(markup, body))) <- results - if Markup.messages.contains(markup.name) - } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body) - - - /* status */ - - def get_status(name: String, status: Query_Operation.Status.Value) - : Option[Query_Operation.Status.Value] = - results.collectFirst({ case XML.Elem(_, List(elem: XML.Elem)) if elem.name == name => status }) - - val new_status = - if (removed) Query_Operation.Status.FINISHED - else - get_status(Markup.FINISHED, Query_Operation.Status.FINISHED) orElse - get_status(Markup.RUNNING, Query_Operation.Status.RUNNING) getOrElse - Query_Operation.Status.WAITING - - if (new_status == Query_Operation.Status.RUNNING) - results.collectFirst( - { - case XML.Elem(Markup(_, Position.Id(id)), List(elem: XML.Elem)) - if elem.name == Markup.RUNNING => id - }).foreach(id => current_exec_id = id) - - - /* state update */ - - if (current_output != new_output || current_status != new_status) { - if (snapshot.is_outdated) - current_update_pending = true - else { - current_update_pending = false - if (current_output != new_output && !removed) { - current_output = new_output - consume_output(snapshot, state.results, new_output) - } - if (current_status != new_status) { - current_status = new_status - consume_status(new_status) - if (new_status == Query_Operation.Status.FINISHED) { - remove_overlay() - PIDE.flush_buffers() - } - } - } - } - } - - - /* query operations */ - - def cancel_query(): Unit = - Swing_Thread.require { PIDE.session.cancel_exec(current_exec_id) } - - def apply_query(query: List[String]) - { - Swing_Thread.require() - - Document_View(view.getTextArea) match { - case Some(doc_view) => - val snapshot = doc_view.model.snapshot() - remove_overlay() - reset_state() - consume_output(Document.State.init.snapshot(), Command.Results.empty, Nil) - snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { - case Some(command) => - current_location = Some(command) - current_query = query - current_status = Query_Operation.Status.WAITING - doc_view.model.insert_overlay(command, operation_name, instance :: query) - case None => - } - consume_status(current_status) - PIDE.flush_buffers() - case None => - } - } - - def locate_query() - { - Swing_Thread.require() - - current_location match { - case Some(command) => - val snapshot = PIDE.document_snapshot(command.node_name) - val commands = snapshot.node.commands - if (commands.contains(command)) { - // FIXME revert offset (!?) - val sources = commands.iterator.takeWhile(_ != command).map(_.source) - val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column) - Hyperlink(command.node_name.node, line, column).follow(view) - } - case None => - } - } - - - /* main actor */ - - private val main_actor = actor { - loop { - react { - case changed: Session.Commands_Changed => - current_location match { - case Some(command) - if current_update_pending || - (current_status != Query_Operation.Status.FINISHED && - changed.commands.contains(command)) => - Swing_Thread.later { content_update() } - case _ => - } - case bad => - java.lang.System.err.println("Query_Operation: ignoring bad message " + bad) - } - } - } - - def activate() { PIDE.session.commands_changed += main_actor } - def deactivate() { PIDE.session.commands_changed -= main_actor } -} diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Mon Aug 12 18:02:01 2013 +0200 @@ -199,15 +199,16 @@ private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH) - def hyperlink(range: Text.Range): Option[Text.Info[Hyperlink]] = + def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] = { - snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include), _ => + snapshot.cumulate_markup[List[Text.Info[PIDE.editor.Hyperlink]]]( + range, Nil, Some(hyperlink_include), _ => { case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) if Path.is_ok(name) => val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name)) - val link = Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) - Some(link :: links) + val link = PIDE.editor.hyperlink_file(jedit_file) + Some(Text.Info(snapshot.convert(info_range), link) :: links) case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) if !props.exists( @@ -220,23 +221,16 @@ Isabelle_System.source_file(Path.explode(name)) match { case Some(path) => val jedit_file = Isabelle_System.platform_path(path) - val link = - Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0)) - Some(link :: links) + val link = PIDE.editor.hyperlink_file(jedit_file, line) + Some(Text.Info(snapshot.convert(info_range), link) :: links) case None => None } case Position.Def_Id_Offset(id, offset) => snapshot.state.find_command(snapshot.version, id) match { case Some((node, command)) => - val sources = - node.commands.iterator.takeWhile(_ != command).map(_.source) ++ - Iterator.single(command.source(Text.Range(0, command.decode(offset)))) - val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column) - val link = - Text.Info(snapshot.convert(info_range), - Hyperlink(command.node_name.node, line, column)) - Some(link :: links) + PIDE.editor.hyperlink_command(snapshot, command, offset) + .map(link => (Text.Info(snapshot.convert(info_range), link) :: links)) case None => None } diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Aug 12 18:02:01 2013 +0200 @@ -135,7 +135,8 @@ private var control: Boolean = false private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _) - private val hyperlink_area = new Active_Area[Hyperlink]((r: Rendering) => r.hyperlink _) + private val hyperlink_area = + new Active_Area[PIDE.editor.Hyperlink]((r: Rendering) => r.hyperlink _) private val active_area = new Active_Area[XML.Elem]((r: Rendering) => r.active _) private val active_areas = diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/sledgehammer_dockable.scala --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Aug 12 18:02:01 2013 +0200 @@ -46,7 +46,7 @@ } private val sledgehammer = - Query_Operation(view, "sledgehammer", consume_status _, + new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status _, (snapshot, results, body) => pretty_text_area.update(snapshot, results, Pretty.separate(body))) diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/text_overview.scala --- a/src/Tools/jEdit/src/text_overview.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/text_overview.scala Mon Aug 12 18:02:01 2013 +0200 @@ -53,7 +53,7 @@ private var cached_colors: List[(Color, Int, Int)] = Nil - private var last_snapshot = Document.State.init.snapshot() + private var last_snapshot = Document.Snapshot.init private var last_options = PIDE.options.value private var last_relevant_range = Text.Range(0) private var last_line_count = 0 diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Mon Aug 12 18:02:01 2013 +0200 @@ -41,7 +41,7 @@ } model.node_required = !model.node_required } } - else if (clicks == 2) Hyperlink(listData(index).node).follow(view) + else if (clicks == 2) PIDE.editor.goto(view, listData(index).node) } case MouseMoved(_, point, _) => val index = peer.locationToIndex(point) @@ -98,7 +98,7 @@ buffer <- JEdit_Lib.jedit_buffers model <- PIDE.document_model(buffer) if model.node_required - } nodes_required += model.name + } nodes_required += model.node_name } update_nodes_required() diff -r 3e0fe71f3ce1 -r 92d98cc6cec2 src/Tools/jEdit/src/timing_dockable.scala --- a/src/Tools/jEdit/src/timing_dockable.scala Mon Aug 12 15:48:57 2013 +0200 +++ b/src/Tools/jEdit/src/timing_dockable.scala Mon Aug 12 18:02:01 2013 +0200 @@ -89,22 +89,14 @@ extends Entry { def print: String = Time.print_seconds(timing) + "s theory " + quote(name.theory) - def follow(snapshot: Document.Snapshot): Unit = Hyperlink(name.node).follow(view) + def follow(snapshot: Document.Snapshot) { PIDE.editor.goto(view, name.node) } } private case class Command_Entry(command: Command, timing: Double) extends Entry { def print: String = " " + Time.print_seconds(timing) + "s command " + quote(command.name) - def follow(snapshot: Document.Snapshot) - { - val node = snapshot.version.nodes(command.node_name) - if (node.commands.contains(command)) { - val sources = node.commands.iterator.takeWhile(_ != command).map(_.source) - val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column) - Hyperlink(command.node_name.node, line, column).follow(view) - } - } + { PIDE.editor.hyperlink_command(snapshot, command).foreach(_.follow(view)) } } @@ -165,7 +157,7 @@ val name = Document_View(view.getTextArea) match { case None => Document.Node.Name.empty - case Some(doc_view) => doc_view.model.name + case Some(doc_view) => doc_view.model.node_name } val timing = nodes_timing.getOrElse(name, Protocol.empty_node_timing)