merged
authorwenzelm
Thu Oct 05 17:39:36 2017 +0200 (20 months ago)
changeset 6676997f16ada519c
parent 66765 c1dfa973b269
parent 66768 f27488f47a47
child 66770 122df1fde073
merged
     1.1 --- a/NEWS	Thu Oct 05 15:35:24 2017 +0100
     1.2 +++ b/NEWS	Thu Oct 05 17:39:36 2017 +0200
     1.3 @@ -30,6 +30,11 @@
     1.4    isabelle build -D '~~/src/ZF'
     1.5  
     1.6  
     1.7 +*** Prover IDE -- Isabelle/Scala/jEdit ***
     1.8 +
     1.9 +* Completion supports theory header imports.
    1.10 +
    1.11 +
    1.12  *** HOL ***
    1.13  
    1.14  * SMT module:
     2.1 --- a/src/Pure/General/completion.scala	Thu Oct 05 15:35:24 2017 +0100
     2.2 +++ b/src/Pure/General/completion.scala	Thu Oct 05 17:39:36 2017 +0200
     2.3 @@ -138,11 +138,22 @@
     2.4      if (s == "" || s == "_") None
     2.5      else Some(s.reverseIterator.dropWhile(_ == '_').toList.reverse.mkString)
     2.6  
     2.7 +  def completed(input: String): String => Boolean =
     2.8 +    clean_name(input) match {
     2.9 +      case None => (name: String) => false
    2.10 +      case Some(prefix) => (name: String) => name.startsWith(prefix)
    2.11 +    }
    2.12 +
    2.13    def report_no_completion(pos: Position.T): String =
    2.14      YXML.string_of_tree(Semantic.Info(pos, No_Completion))
    2.15  
    2.16 -  def report_names(pos: Position.T, total: Int, names: List[(String, (String, String))]): String =
    2.17 -    YXML.string_of_tree(Semantic.Info(pos, Names(total, names)))
    2.18 +  def report_names(pos: Position.T, names: List[(String, (String, String))], total: Int = 0): String =
    2.19 +    if (names.isEmpty) ""
    2.20 +    else
    2.21 +      YXML.string_of_tree(Semantic.Info(pos, Names(if (total > 0) total else names.length, names)))
    2.22 +
    2.23 +  def report_theories(pos: Position.T, thys: List[String], total: Int = 0): String =
    2.24 +    report_names(pos, thys.map(name => (name, ("theory", name))), total)
    2.25  
    2.26    object Semantic
    2.27    {
     3.1 --- a/src/Pure/PIDE/command.scala	Thu Oct 05 15:35:24 2017 +0100
     3.2 +++ b/src/Pure/PIDE/command.scala	Thu Oct 05 17:39:36 2017 +0200
     3.3 @@ -438,12 +438,32 @@
     3.4        // inlined errors
     3.5        case Thy_Header.THEORY =>
     3.6          val reader = Scan.char_reader(Token.implode(span.content))
     3.7 -        val header = resources.check_thy_reader(node_name, reader)
     3.8 +        val imports = resources.check_thy_reader(node_name, reader).imports
     3.9 +        val raw_imports =
    3.10 +          try {
    3.11 +            val imports1 = Thy_Header.read(reader, Token.Pos.none).imports
    3.12 +            if (imports.length == imports1.length) imports1.map(_._1) else error("")
    3.13 +          }
    3.14 +          catch { case exn: Throwable => List.fill(imports.length)("") }
    3.15 +
    3.16          val errors =
    3.17 -          for ((imp, pos) <- header.imports if !can_import(imp)) yield {
    3.18 +          for { ((import_name, pos), s) <- imports zip raw_imports if !can_import(import_name) }
    3.19 +          yield {
    3.20 +            val completion =
    3.21 +              if (Thy_Header.is_base_name(s)) {
    3.22 +                val completed = Completion.completed(import_name.theory_base_name)
    3.23 +                val qualifier = resources.theory_qualifier(node_name)
    3.24 +                val dir = node_name.master_dir
    3.25 +                for {
    3.26 +                  (_, known_name) <- resources.session_base.known.theories.toList
    3.27 +                  if completed(known_name.theory_base_name)
    3.28 +                } yield resources.standard_import(resources, qualifier, dir, known_name.theory)
    3.29 +              }.sorted
    3.30 +              else Nil
    3.31              val msg =
    3.32                "Bad theory import " +
    3.33 -                Markup.Path(imp.node).markup(quote(imp.toString)) + Position.here(pos)
    3.34 +                Markup.Path(import_name.node).markup(quote(import_name.toString)) +
    3.35 +                Position.here(pos) + Completion.report_theories(pos, completion)
    3.36              Exn.Exn(ERROR(msg)): Command.Blob
    3.37            }
    3.38          (errors, -1)
     4.1 --- a/src/Pure/PIDE/resources.scala	Thu Oct 05 15:35:24 2017 +0100
     4.2 +++ b/src/Pure/PIDE/resources.scala	Thu Oct 05 17:39:36 2017 +0200
     4.3 @@ -115,6 +115,25 @@
     4.4    def import_name(name: Document.Node.Name, s: String): Document.Node.Name =
     4.5      import_name(theory_qualifier(name), name.master_dir, s)
     4.6  
     4.7 +  def standard_import(session_resources: Resources,
     4.8 +    qualifier: String, dir: String, s: String): String =
     4.9 +  {
    4.10 +    val name = import_name(qualifier, dir, s)
    4.11 +    val s1 =
    4.12 +      if (session_base.loaded_theory(name)) name.theory
    4.13 +      else {
    4.14 +        session_base.known.get_file(name.path.file) match {
    4.15 +          case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    4.16 +            name1.theory
    4.17 +          case Some(name1) if Thy_Header.is_base_name(s) =>
    4.18 +            name1.theory_base_name
    4.19 +          case _ => s
    4.20 +        }
    4.21 +      }
    4.22 +    val name2 = import_name(qualifier, dir, s1)
    4.23 +    if (name.node == name2.node) s1 else s
    4.24 +  }
    4.25 +
    4.26    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    4.27    {
    4.28      val path = File.check_file(name.path)
    4.29 @@ -134,7 +153,7 @@
    4.30          if (base_name != name)
    4.31            error("Bad theory name " + quote(name) +
    4.32              " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
    4.33 -            Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
    4.34 +            Completion.report_theories(pos, List(base_name)))
    4.35  
    4.36          val imports = header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
    4.37          Document.Node.Header(imports, header.keywords, header.abbrevs)
     5.1 --- a/src/Pure/Tools/imports.scala	Thu Oct 05 15:35:24 2017 +0100
     5.2 +++ b/src/Pure/Tools/imports.scala	Thu Oct 05 17:39:36 2017 +0200
     5.3 @@ -141,22 +141,7 @@
     5.4            val imports_resources = new Resources(imports_base)
     5.5  
     5.6            def standard_import(qualifier: String, dir: String, s: String): String =
     5.7 -          {
     5.8 -            val name = imports_resources.import_name(qualifier, dir, s)
     5.9 -            val s1 =
    5.10 -              if (imports_base.loaded_theory(name)) name.theory
    5.11 -              else {
    5.12 -                imports_base.known.get_file(name.path.file) match {
    5.13 -                  case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    5.14 -                    name1.theory
    5.15 -                  case Some(name1) if Thy_Header.is_base_name(s) =>
    5.16 -                    name1.theory_base_name
    5.17 -                  case _ => s
    5.18 -                }
    5.19 -              }
    5.20 -            val name2 = imports_resources.import_name(qualifier, dir, s1)
    5.21 -            if (name.node == name2.node) s1 else s
    5.22 -          }
    5.23 +            imports_resources.standard_import(session_resources, qualifier, dir, s)
    5.24  
    5.25            val updates_root =
    5.26              for {