discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
authorwenzelm
Thu Sep 28 11:53:55 2017 +0200 (2017-09-28 ago)
changeset 6671180fa1401cf76
parent 66706 0b9e6ce3b843
child 66712 4c98c929a12a
discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;
src/Pure/PIDE/resources.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_info.scala
     1.1 --- a/src/Pure/PIDE/resources.ML	Thu Sep 28 09:42:28 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Thu Sep 28 11:53:55 2017 +0200
     1.3 @@ -20,8 +20,7 @@
     1.4    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
     1.5    val thy_path: Path.T -> Path.T
     1.6    val theory_qualifier: string -> string
     1.7 -  val import_name: string -> Path.T -> string ->
     1.8 -    {node_name: Path.T, master_dir: Path.T, theory_name: string}
     1.9 +  val import_name: string -> Path.T -> string -> {master_dir: Path.T, theory_name: string}
    1.10    val check_thy: Path.T -> string ->
    1.11     {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
    1.12      imports: (string * Position.T) list, keywords: Thy_Header.keywords}
    1.13 @@ -120,14 +119,13 @@
    1.14  
    1.15  fun import_name qualifier dir s =
    1.16    (case theory_name qualifier (Thy_Header.import_name s) of
    1.17 -    (true, theory) =>
    1.18 -      {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}
    1.19 +    (true, theory) => {master_dir = Path.current, theory_name = theory}
    1.20    | (false, theory) =>
    1.21        let val node_name =
    1.22          (case known_theory theory of
    1.23            SOME node_name => node_name
    1.24          | NONE => File.full_path dir (thy_path (Path.expand (Path.explode s))))
    1.25 -      in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end);
    1.26 +      in {master_dir = Path.dir node_name, theory_name = theory} end);
    1.27  
    1.28  fun check_file dir file = File.check_file (File.full_path dir file);
    1.29  
     2.1 --- a/src/Pure/Thy/thy_info.ML	Thu Sep 28 09:42:28 2017 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Sep 28 11:53:55 2017 +0200
     2.3 @@ -160,7 +160,7 @@
     2.4    in res :: map Exn.Exn exns end;
     2.5  
     2.6  datatype task =
     2.7 -  Task of Path.T * string list * (theory list -> result) |
     2.8 +  Task of string list * (theory list -> result) |
     2.9    Finished of theory;
    2.10  
    2.11  fun task_finished (Task _) = false
    2.12 @@ -171,7 +171,7 @@
    2.13  val schedule_seq =
    2.14    String_Graph.schedule (fn deps => fn (_, task) =>
    2.15      (case task of
    2.16 -      Task (_, parents, body) =>
    2.17 +      Task (parents, body) =>
    2.18          let
    2.19            val result = body (task_parents deps parents);
    2.20            val _ = Par_Exn.release_all (join_theory result);
    2.21 @@ -185,7 +185,7 @@
    2.22      val futures = tasks
    2.23        |> String_Graph.schedule (fn deps => fn (name, task) =>
    2.24          (case task of
    2.25 -          Task (_, parents, body) =>
    2.26 +          Task (parents, body) =>
    2.27              (singleton o Future.forks)
    2.28                {name = "theory:" ^ name, group = NONE,
    2.29                  deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
    2.30 @@ -335,19 +335,10 @@
    2.31        |>> forall I
    2.32  and require_thy document symbols last_timing initiators qualifier dir (s, require_pos) tasks =
    2.33    let
    2.34 -    val {node_name, master_dir, theory_name} = Resources.import_name qualifier dir s;
    2.35 -    fun check_entry (Task (node_name', _, _)) =
    2.36 -          if op = (apply2 File.platform_path (node_name, node_name'))
    2.37 -          then ()
    2.38 -          else
    2.39 -            error ("Incoherent imports for theory " ^ quote theory_name ^
    2.40 -              Position.here require_pos ^ ":\n" ^
    2.41 -              "  " ^ Path.print node_name ^ "\n" ^
    2.42 -              "  " ^ Path.print node_name')
    2.43 -      | check_entry _ = ();
    2.44 +    val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s;
    2.45    in
    2.46      (case try (String_Graph.get_node tasks) theory_name of
    2.47 -      SOME task => (check_entry task; (task_finished task, tasks))
    2.48 +      SOME task => (task_finished task, tasks)
    2.49      | NONE =>
    2.50          let
    2.51            val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
    2.52 @@ -378,7 +369,7 @@
    2.53                      val load =
    2.54                        load_thy document symbols last_timing initiators update_time dep
    2.55                          text (theory_name, theory_pos) keywords;
    2.56 -                  in Task (node_name, parents, load) end);
    2.57 +                  in Task (parents, load) end);
    2.58  
    2.59            val tasks'' = new_entry theory_name parents task tasks';
    2.60          in (all_current, tasks'') end)
     3.1 --- a/src/Pure/Thy/thy_info.scala	Thu Sep 28 09:42:28 2017 +0200
     3.2 +++ b/src/Pure/Thy/thy_info.scala	Thu Sep 28 11:53:55 2017 +0200
     3.3 @@ -38,44 +38,25 @@
     3.4  
     3.5    object Dependencies
     3.6    {
     3.7 -    val empty = new Dependencies(Nil, Nil, Nil, Set.empty, Multi_Map.empty)
     3.8 +    val empty = new Dependencies(Nil, Nil, Nil, Set.empty)
     3.9    }
    3.10  
    3.11    final class Dependencies private(
    3.12      rev_deps: List[Thy_Info.Dep],
    3.13      val keywords: Thy_Header.Keywords,
    3.14      val abbrevs: Thy_Header.Abbrevs,
    3.15 -    val seen: Set[Document.Node.Name],
    3.16 -    val seen_theory: Multi_Map[String, (Document.Node.Name, Position.T)])
    3.17 +    val seen: Set[Document.Node.Name])
    3.18    {
    3.19      def :: (dep: Thy_Info.Dep): Dependencies =
    3.20        new Dependencies(
    3.21 -        dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs,
    3.22 -        seen, seen_theory)
    3.23 +        dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs, seen)
    3.24  
    3.25 -    def + (thy: (Document.Node.Name, Position.T)): Dependencies =
    3.26 -    {
    3.27 -      val (name, _) = thy
    3.28 -      new Dependencies(rev_deps, keywords, abbrevs, seen + name, seen_theory + (name.theory -> thy))
    3.29 -    }
    3.30 +    def + (name: Document.Node.Name): Dependencies =
    3.31 +      new Dependencies(rev_deps, keywords, abbrevs, seen + name)
    3.32  
    3.33      def deps: List[Thy_Info.Dep] = rev_deps.reverse
    3.34  
    3.35 -    def errors: List[String] =
    3.36 -    {
    3.37 -      val header_errors = deps.flatMap(dep => dep.header.errors)
    3.38 -      val import_errors =
    3.39 -        (for {
    3.40 -          (theory, imports) <- seen_theory.iterator_list
    3.41 -          if !resources.session_base.loaded_theories.isDefinedAt(theory)
    3.42 -          if imports.length > 1
    3.43 -        } yield {
    3.44 -          "Incoherent imports for theory " + quote(theory) + ":\n" +
    3.45 -            cat_lines(imports.map({ case (name, pos) =>
    3.46 -              "  " + quote(name.node) + Position.here(pos) }))
    3.47 -        }).toList
    3.48 -      header_errors ::: import_errors
    3.49 -    }
    3.50 +    def errors: List[String] = deps.flatMap(dep => dep.header.errors)
    3.51  
    3.52      lazy val syntax: Outer_Syntax =
    3.53        resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
    3.54 @@ -105,13 +86,13 @@
    3.55    private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
    3.56      thy: (Document.Node.Name, Position.T)): Dependencies =
    3.57    {
    3.58 -    val (name, require_pos) = thy
    3.59 +    val (name, pos) = thy
    3.60  
    3.61      def message: String =
    3.62        "The error(s) above occurred for theory " + quote(name.theory) +
    3.63 -        required_by(initiators) + Position.here(require_pos)
    3.64 +        required_by(initiators) + Position.here(pos)
    3.65  
    3.66 -    val required1 = required + thy
    3.67 +    val required1 = required + name
    3.68      if (required.seen(name)) required
    3.69      else if (resources.session_base.loaded_theory(name)) required1
    3.70      else {