# HG changeset patch # User wenzelm # Date 1507217976 -7200 # Node ID 97f16ada519c26205f989b3158b695c736191749 # Parent c1dfa973b26966cb0fd49824c38a04acb5fadb71# Parent f27488f47a47219b35038d9d87ad6937631d586d merged diff -r c1dfa973b269 -r 97f16ada519c NEWS --- 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: diff -r c1dfa973b269 -r 97f16ada519c src/Pure/General/completion.scala --- 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 { diff -r c1dfa973b269 -r 97f16ada519c src/Pure/PIDE/command.scala --- 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) diff -r c1dfa973b269 -r 97f16ada519c src/Pure/PIDE/resources.scala --- 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) diff -r c1dfa973b269 -r 97f16ada519c src/Pure/Tools/imports.scala --- 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 {