38 |
38 |
39 object Known |
39 object Known |
40 { |
40 { |
41 val empty: Known = Known() |
41 val empty: Known = Known() |
42 |
42 |
43 def make(local_dir: Path, bases: List[Base], |
43 def make(bases: List[Base], |
44 theories: List[Document.Node.Entry] = Nil, |
44 theories: List[Document.Node.Entry] = Nil, |
45 loaded_files: List[(String, List[Path])] = Nil): Known = |
45 loaded_files: List[(String, List[Path])] = Nil): Known = |
46 { |
46 { |
47 def bases_iterator(local: Boolean) = |
47 def bases_theories_iterator = |
48 for { |
48 for { |
49 base <- bases.iterator |
49 base <- bases.iterator |
50 (_, entry) <- (if (local) base.known.theories_local else base.known.theories).iterator |
50 (_, entry) <- base.known.theories.iterator |
51 } yield entry |
51 } yield entry |
52 |
52 |
53 def local_theories_iterator = |
|
54 { |
|
55 val local_path = local_dir.canonical_file.toPath |
|
56 theories.iterator.filter(entry => |
|
57 entry.name.path.canonical_file.toPath.startsWith(local_path)) |
|
58 } |
|
59 |
|
60 val known_theories = |
53 val known_theories = |
61 (Map.empty[String, Document.Node.Entry] /: (bases_iterator(false) ++ theories.iterator))({ |
54 (Map.empty[String, Document.Node.Entry] /: (bases_theories_iterator ++ theories.iterator))({ |
62 case (known, entry) => |
55 case (known, entry) => |
63 known.get(entry.name.theory) match { |
56 known.get(entry.name.theory) match { |
64 case Some(entry1) if entry.name != entry1.name => |
57 case Some(entry1) if entry.name != entry1.name => |
65 error("Duplicate theory " + quote(entry.name.node) + " vs. " + |
58 error("Duplicate theory " + quote(entry.name.node) + " vs. " + |
66 quote(entry1.name.node)) |
59 quote(entry1.name.node)) |
67 case _ => known + (entry.name.theory -> entry) |
60 case _ => known + (entry.name.theory -> entry) |
68 } |
61 } |
69 }) |
62 }) |
70 val known_theories_local = |
|
71 (Map.empty[String, Document.Node.Entry] /: |
|
72 (bases_iterator(true) ++ local_theories_iterator))({ |
|
73 case (known, entry) => known + (entry.name.theory -> entry) |
|
74 }) |
|
75 val known_files = |
|
76 (Map.empty[JFile, List[Document.Node.Name]] /: |
|
77 (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({ |
|
78 case (known, entry) => |
|
79 val name = entry.name |
|
80 val file = name.path.canonical_file |
|
81 val theories1 = known.getOrElse(file, Nil) |
|
82 if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory)) |
|
83 known |
|
84 else known + (file -> (name :: theories1)) |
|
85 }) |
|
86 |
63 |
87 val known_loaded_files = |
64 val known_loaded_files = |
88 (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _) |
65 (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _) |
89 |
66 |
90 Known( |
67 Known(known_theories, known_loaded_files) |
91 known_theories, |
|
92 known_theories_local, |
|
93 known_files.iterator.map(p => (p._1, p._2.reverse)).toMap, |
|
94 known_loaded_files) |
|
95 } |
68 } |
96 } |
69 } |
97 |
70 |
98 sealed case class Known( |
71 sealed case class Known( |
99 theories: Map[String, Document.Node.Entry] = Map.empty, |
72 theories: Map[String, Document.Node.Entry] = Map.empty, |
100 theories_local: Map[String, Document.Node.Entry] = Map.empty, |
|
101 files: Map[JFile, List[Document.Node.Name]] = Map.empty, |
|
102 loaded_files: Map[String, List[Path]] = Map.empty) |
73 loaded_files: Map[String, List[Path]] = Map.empty) |
103 { |
74 { |
104 def platform_path: Known = |
75 def platform_path: Known = |
105 copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))), |
76 copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_)))) |
106 theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.platform_path(_))), |
|
107 files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.platform_path(_))))) |
|
108 |
77 |
109 def standard_path: Known = |
78 def standard_path: Known = |
110 copy(theories = for ((a, b) <- theories) yield (a, b.map(File.standard_path(_))), |
79 copy(theories = for ((a, b) <- theories) yield (a, b.map(File.standard_path(_)))) |
111 theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.standard_path(_))), |
|
112 files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.standard_path(_))))) |
|
113 |
|
114 def theory_names: List[Document.Node.Name] = theories.iterator.map(p => p._2.name).toList |
|
115 |
|
116 lazy val theory_graph: Document.Node.Name.Graph[Unit] = |
|
117 Document.Node.Name.make_graph( |
|
118 for ((_, entry) <- theories.toList) |
|
119 yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp.theory).name))) |
|
120 |
|
121 def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] = |
|
122 { |
|
123 val res = files.getOrElse(File.canonical(file), Nil).headOption |
|
124 if (bootstrap) res.map(_.map_theory(Thy_Header.bootstrap_name(_))) else res |
|
125 } |
|
126 } |
80 } |
127 |
81 |
128 object Base |
82 object Base |
129 { |
83 { |
130 def bootstrap( |
84 def bootstrap( |