--- a/NEWS Fri Dec 18 12:57:25 2020 +0100
+++ b/NEWS Fri Dec 18 23:19:07 2020 +0100
@@ -16,6 +16,9 @@
*** Isabelle/jEdit Prover IDE ***
+* Improved markup for theory header imports: hyperlinks for theory files
+work without formal checking of content.
+
* Action "isabelle.goto-entity" (shortcut CS+d) jumps to the definition
of the formal entity at the caret position.
--- a/src/Pure/PIDE/command.scala Fri Dec 18 12:57:25 2020 +0100
+++ b/src/Pure/PIDE/command.scala Fri Dec 18 23:19:07 2020 +0100
@@ -445,8 +445,8 @@
span.name match {
// inlined errors
case Thy_Header.THEORY =>
- val reader = Scan.char_reader(Token.implode(span.content))
- val header = resources.check_thy(node_name, reader)
+ val reader = span.content_reader
+ val header = resources.check_thy(node_name, span.content_reader)
val imports_pos = header.imports_pos
val raw_imports =
try {
@@ -567,6 +567,23 @@
def source(range: Text.Range): String = range.substring(source)
+ /* theory parents */
+
+ def theory_parents(resources: Resources): List[Document.Node.Name] =
+ if (span.name == Thy_Header.THEORY) {
+ try {
+ val header = Thy_Header.read(node_name, span.content_reader)
+ for ((s, _) <- header.imports)
+ yield {
+ try { resources.import_name(node_name, s) }
+ catch { case ERROR(_) => Document.Node.Name.empty }
+ }
+ }
+ catch { case ERROR(_) => Nil }
+ }
+ else Nil
+
+
/* reported positions */
def reported_position(pos: Position.T)
--- a/src/Pure/PIDE/command_span.scala Fri Dec 18 12:57:25 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala Fri Dec 18 23:19:07 2020 +0100
@@ -8,6 +8,7 @@
import scala.collection.mutable
+import scala.util.parsing.input.CharSequenceReader
object Command_Span
@@ -89,6 +90,8 @@
def is_begin: Boolean = content.exists(_.is_begin)
def is_end: Boolean = content.exists(_.is_end)
+ def content_reader: CharSequenceReader = Scan.char_reader(Token.implode(content))
+
def length: Int = (0 /: content)(_ + _.source.length)
def compact_source: (String, Span) =
--- a/src/Pure/PIDE/document.ML Fri Dec 18 12:57:25 2020 +0100
+++ b/src/Pure/PIDE/document.ML Fri Dec 18 23:19:07 2020 +0100
@@ -22,6 +22,7 @@
type command =
{command_id: Document_ID.command,
name: string,
+ parents: string list,
blobs_digests: blob_digest list,
blobs_index: int,
tokens: ((int * int) * string) list}
@@ -410,11 +411,12 @@
type command =
{command_id: Document_ID.command,
name: string,
+ parents: string list,
blobs_digests: blob_digest list,
blobs_index: int,
tokens: ((int * int) * string) list};
-fun define_command {command_id, name, blobs_digests, blobs_index, tokens} =
+fun define_command {command_id, name, parents, blobs_digests, blobs_index, tokens} =
map_state (fn (versions, blobs, commands, execution) =>
let
val id = Document_ID.print command_id;
@@ -424,6 +426,23 @@
(fn () =>
let
val (tokens, _) = fold_map Token.make tokens (Position.id id);
+ val imports =
+ if name = Thy_Header.theoryN then
+ #imports (Thy_Header.read_tokens Position.none tokens)
+ else [];
+ val _ =
+ if length parents = length imports then
+ (parents, imports) |> ListPair.app (fn (parent, (_, pos)) =>
+ let val markup =
+ (case Thy_Info.lookup_theory parent of
+ SOME thy => Theory.get_markup thy
+ | NONE =>
+ (case try Url.explode parent of
+ NONE => Markup.path parent
+ | SOME (Url.File path) => Markup.path (Path.implode path)
+ | SOME _ => Markup.url parent))
+ in Position.report pos markup end)
+ else ();
val _ =
if blobs_index < 0
then (*inlined errors*)
@@ -598,8 +617,8 @@
(case get_result (snd (the (AList.lookup (op =) deps import))) of
NONE => Toplevel.init_toplevel ()
| SOME (_, eval) => maybe_eval_result eval)
- | some => some)
- |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy))));
+ |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy)))
+ | SOME thy => SOME (thy, (Position.none, Markup.empty))));
val parents =
if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports;
--- a/src/Pure/PIDE/protocol.ML Fri Dec 18 12:57:25 2020 +0100
+++ b/src/Pure/PIDE/protocol.ML Fri Dec 18 23:19:07 2020 +0100
@@ -31,9 +31,10 @@
Isabelle_Process.protocol_command "Document.define_blob"
(fn [digest, content] => Document.change_state (Document.define_blob digest content));
-fun decode_command id name blobs_xml toks_xml sources : Document.command =
+fun decode_command id name parents_xml blobs_xml toks_xml sources : Document.command =
let
open XML.Decode;
+ val parents = list string parents_xml;
val (blobs_digests, blobs_index) =
blobs_xml |>
let
@@ -52,6 +53,7 @@
in
{command_id = Document_ID.parse id,
name = name,
+ parents = parents,
blobs_digests = blobs_digests,
blobs_index = blobs_index,
tokens = toks ~~ sources}
@@ -62,9 +64,11 @@
val _ =
Isabelle_Process.protocol_command "Document.define_command"
- (fn id :: name :: blobs :: toks :: sources =>
+ (fn id :: name :: parents :: blobs :: toks :: sources =>
let
- val command = decode_command id name (YXML.parse_body blobs) (YXML.parse_body toks) sources;
+ val command =
+ decode_command id name (YXML.parse_body parents) (YXML.parse_body blobs)
+ (YXML.parse_body toks) sources;
val _ = Document.change_state (Document.define_command command);
in commands_accepted [id] end);
@@ -75,9 +79,10 @@
fun decode arg =
let
open XML.Decode;
- val (id, (name, (blobs_xml, (toks_xml, sources)))) =
- pair string (pair string (pair I (pair I (list string)))) (YXML.parse_body arg);
- in decode_command id name blobs_xml toks_xml sources end;
+ val (id, (name, (parents_xml, (blobs_xml, (toks_xml, sources))))) =
+ pair string (pair string (pair I (pair I (pair I (list string)))))
+ (YXML.parse_body arg);
+ in decode_command id name parents_xml blobs_xml toks_xml sources end;
val commands = map decode args;
val _ = Document.change_state (fold Document.define_command commands);
--- a/src/Pure/PIDE/protocol.scala Fri Dec 18 12:57:25 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala Fri Dec 18 23:19:07 2020 +0100
@@ -321,10 +321,14 @@
def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
protocol_command_raw("Document.define_blob", List(Bytes(digest.toString), bytes))
- private def encode_command(command: Command): (String, String, String, String, List[String]) =
+ private def encode_command(resources: Resources, command: Command)
+ : (String, String, String, String, String, List[String]) =
{
import XML.Encode._
+ val parents = command.theory_parents(resources).map(name => File.standard_url(name.node))
+ val parents_yxml = Symbol.encode_yxml(list(string)(parents))
+
val blobs_yxml =
{
val encode_blob: T[Exn.Result[Command.Blob]] =
@@ -344,38 +348,42 @@
}
val toks_sources = command.span.content.map(tok => Symbol.encode(tok.source))
- (Document_ID(command.id), Symbol.encode(command.span.name), blobs_yxml, toks_yxml, toks_sources)
+ (Document_ID(command.id), Symbol.encode(command.span.name), parents_yxml,
+ blobs_yxml, toks_yxml, toks_sources)
}
- def define_command(command: Command)
+ def define_command(resources: Resources, command: Command)
{
- val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command)
+ val (command_id, name, parents_yxml, blobs_yxml, toks_yxml, toks_sources) =
+ encode_command(resources, command)
protocol_command_args(
- "Document.define_command", command_id :: name :: blobs_yxml :: toks_yxml :: toks_sources)
+ "Document.define_command", command_id :: name :: parents_yxml :: blobs_yxml ::
+ toks_yxml :: toks_sources)
}
- def define_commands(commands: List[Command])
+ def define_commands(resources: Resources, commands: List[Command])
{
protocol_command_args("Document.define_commands",
commands.map(command =>
{
import XML.Encode._
- val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command)
+ val (command_id, name, parents_yxml, blobs_yxml, toks_yxml, toks_sources) =
+ encode_command(resources, command)
val body =
- pair(string, pair(string, pair(string, pair(string, list(string)))))(
- command_id, (name, (blobs_yxml, (toks_yxml, toks_sources))))
+ pair(string, pair(string, pair(string, pair(string, pair(string, list(string))))))(
+ command_id, (name, (parents_yxml, (blobs_yxml, (toks_yxml, toks_sources)))))
YXML.string_of_body(body)
}))
}
- def define_commands_bulk(commands: List[Command])
+ def define_commands_bulk(resources: Resources, commands: List[Command])
{
val (irregular, regular) = commands.partition(command => YXML.detect(command.source))
- irregular.foreach(define_command)
+ irregular.foreach(define_command(resources, _))
regular match {
case Nil =>
- case List(command) => define_command(command)
- case _ => define_commands(regular)
+ case List(command) => define_command(resources, command)
+ case _ => define_commands(resources, regular)
}
}
--- a/src/Pure/PIDE/session.scala Fri Dec 18 12:57:25 2020 +0100
+++ b/src/Pure/PIDE/session.scala Fri Dec 18 23:19:07 2020 +0100
@@ -452,7 +452,9 @@
for { (_, edit) <- change.doc_edits } {
edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) })
}
- if (id_commands.nonEmpty) prover.get.define_commands_bulk(id_commands.toList)
+ if (id_commands.nonEmpty) {
+ prover.get.define_commands_bulk(resources, id_commands.toList)
+ }
}
val assignment = global_state.value.the_assignment(change.previous).check_finished