# HG changeset patch
# User wenzelm
# Date 1608329947 -3600
# Node ID 9329abcdd651d7ff65a19c7af478dec4134e9e39
# Parent  756b9cb8a17665c5ac66327cb2f0a7d2deaf3d58
improved markup for theory header imports;

diff -r 756b9cb8a176 -r 9329abcdd651 NEWS
--- 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.
 
diff -r 756b9cb8a176 -r 9329abcdd651 src/Pure/PIDE/command.scala
--- 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)
diff -r 756b9cb8a176 -r 9329abcdd651 src/Pure/PIDE/command_span.scala
--- 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) =
diff -r 756b9cb8a176 -r 9329abcdd651 src/Pure/PIDE/document.ML
--- 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;
diff -r 756b9cb8a176 -r 9329abcdd651 src/Pure/PIDE/protocol.ML
--- 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);
diff -r 756b9cb8a176 -r 9329abcdd651 src/Pure/PIDE/protocol.scala
--- 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)
     }
   }
 
diff -r 756b9cb8a176 -r 9329abcdd651 src/Pure/PIDE/session.scala
--- 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