--- a/NEWS Thu Oct 05 15:35:24 2017 +0100
+++ b/NEWS Thu Oct 05 17:39:36 2017 +0200
@@ -30,6 +30,11 @@
isabelle build -D '~~/src/ZF'
+*** Prover IDE -- Isabelle/Scala/jEdit ***
+
+* Completion supports theory header imports.
+
+
*** HOL ***
* SMT module:
--- a/src/Pure/General/completion.scala Thu Oct 05 15:35:24 2017 +0100
+++ b/src/Pure/General/completion.scala Thu Oct 05 17:39:36 2017 +0200
@@ -138,11 +138,22 @@
if (s == "" || s == "_") None
else Some(s.reverseIterator.dropWhile(_ == '_').toList.reverse.mkString)
+ def completed(input: String): String => Boolean =
+ clean_name(input) match {
+ case None => (name: String) => false
+ case Some(prefix) => (name: String) => name.startsWith(prefix)
+ }
+
def report_no_completion(pos: Position.T): String =
YXML.string_of_tree(Semantic.Info(pos, No_Completion))
- def report_names(pos: Position.T, total: Int, names: List[(String, (String, String))]): String =
- YXML.string_of_tree(Semantic.Info(pos, Names(total, names)))
+ def report_names(pos: Position.T, names: List[(String, (String, String))], total: Int = 0): String =
+ if (names.isEmpty) ""
+ else
+ YXML.string_of_tree(Semantic.Info(pos, Names(if (total > 0) total else names.length, names)))
+
+ def report_theories(pos: Position.T, thys: List[String], total: Int = 0): String =
+ report_names(pos, thys.map(name => (name, ("theory", name))), total)
object Semantic
{
--- a/src/Pure/PIDE/command.scala Thu Oct 05 15:35:24 2017 +0100
+++ b/src/Pure/PIDE/command.scala Thu Oct 05 17:39:36 2017 +0200
@@ -438,12 +438,32 @@
// inlined errors
case Thy_Header.THEORY =>
val reader = Scan.char_reader(Token.implode(span.content))
- val header = resources.check_thy_reader(node_name, reader)
+ val imports = resources.check_thy_reader(node_name, reader).imports
+ val raw_imports =
+ try {
+ val imports1 = Thy_Header.read(reader, Token.Pos.none).imports
+ if (imports.length == imports1.length) imports1.map(_._1) else error("")
+ }
+ catch { case exn: Throwable => List.fill(imports.length)("") }
+
val errors =
- for ((imp, pos) <- header.imports if !can_import(imp)) yield {
+ for { ((import_name, pos), s) <- imports zip raw_imports if !can_import(import_name) }
+ yield {
+ val completion =
+ if (Thy_Header.is_base_name(s)) {
+ val completed = Completion.completed(import_name.theory_base_name)
+ val qualifier = resources.theory_qualifier(node_name)
+ val dir = node_name.master_dir
+ for {
+ (_, known_name) <- resources.session_base.known.theories.toList
+ if completed(known_name.theory_base_name)
+ } yield resources.standard_import(resources, qualifier, dir, known_name.theory)
+ }.sorted
+ else Nil
val msg =
"Bad theory import " +
- Markup.Path(imp.node).markup(quote(imp.toString)) + Position.here(pos)
+ Markup.Path(import_name.node).markup(quote(import_name.toString)) +
+ Position.here(pos) + Completion.report_theories(pos, completion)
Exn.Exn(ERROR(msg)): Command.Blob
}
(errors, -1)
--- a/src/Pure/PIDE/resources.scala Thu Oct 05 15:35:24 2017 +0100
+++ b/src/Pure/PIDE/resources.scala Thu Oct 05 17:39:36 2017 +0200
@@ -115,6 +115,25 @@
def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
import_name(theory_qualifier(name), name.master_dir, s)
+ def standard_import(session_resources: Resources,
+ qualifier: String, dir: String, s: String): String =
+ {
+ val name = import_name(qualifier, dir, s)
+ val s1 =
+ if (session_base.loaded_theory(name)) name.theory
+ else {
+ session_base.known.get_file(name.path.file) match {
+ case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
+ name1.theory
+ case Some(name1) if Thy_Header.is_base_name(s) =>
+ name1.theory_base_name
+ case _ => s
+ }
+ }
+ val name2 = import_name(qualifier, dir, s1)
+ if (name.node == name2.node) s1 else s
+ }
+
def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
{
val path = File.check_file(name.path)
@@ -134,7 +153,7 @@
if (base_name != name)
error("Bad theory name " + quote(name) +
" for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
- Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
+ Completion.report_theories(pos, List(base_name)))
val imports = header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
Document.Node.Header(imports, header.keywords, header.abbrevs)
--- a/src/Pure/Tools/imports.scala Thu Oct 05 15:35:24 2017 +0100
+++ b/src/Pure/Tools/imports.scala Thu Oct 05 17:39:36 2017 +0200
@@ -141,22 +141,7 @@
val imports_resources = new Resources(imports_base)
def standard_import(qualifier: String, dir: String, s: String): String =
- {
- val name = imports_resources.import_name(qualifier, dir, s)
- val s1 =
- if (imports_base.loaded_theory(name)) name.theory
- else {
- imports_base.known.get_file(name.path.file) match {
- case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
- name1.theory
- case Some(name1) if Thy_Header.is_base_name(s) =>
- name1.theory_base_name
- case _ => s
- }
- }
- val name2 = imports_resources.import_name(qualifier, dir, s1)
- if (name.node == name2.node) s1 else s
- }
+ imports_resources.standard_import(session_resources, qualifier, dir, s)
val updates_root =
for {