26 |
26 |
27 type Dep = (Document.Node.Name, Document.Node.Header) |
27 type Dep = (Document.Node.Name, Document.Node.Header) |
28 |
28 |
29 object Dependencies |
29 object Dependencies |
30 { |
30 { |
31 val empty = new Dependencies(Nil, Set.empty) |
31 val empty = new Dependencies(Nil, Nil, Set.empty) |
32 } |
32 } |
33 |
33 |
34 final class Dependencies private( |
34 final class Dependencies private( |
35 rev_deps: List[Dep], |
35 rev_deps: List[Dep], |
|
36 val keywords: Thy_Header.Keywords, |
36 val seen: Set[Document.Node.Name]) |
37 val seen: Set[Document.Node.Name]) |
37 { |
38 { |
38 def :: (dep: Dep): Dependencies = new Dependencies(dep :: rev_deps, seen) |
39 def :: (dep: Dep): Dependencies = |
39 def + (name: Document.Node.Name): Dependencies = new Dependencies(rev_deps, seen = seen + name) |
40 new Dependencies(dep :: rev_deps, dep._2.keywords ::: keywords, seen) |
|
41 |
|
42 def + (name: Document.Node.Name): Dependencies = |
|
43 new Dependencies(rev_deps, keywords, seen = seen + name) |
40 |
44 |
41 def deps: List[Dep] = rev_deps.reverse |
45 def deps: List[Dep] = rev_deps.reverse |
42 |
46 |
43 def thy_load_commands: List[String] = |
47 def thy_load_commands: List[String] = |
44 (for ((_, h) <- rev_deps; (cmd, Some(((Keyword.THY_LOAD, _), _))) <- h.keywords) yield cmd) ::: |
48 (for ((cmd, Some(((Keyword.THY_LOAD, _), _))) <- keywords) yield cmd) ::: |
45 thy_load.base_syntax.thy_load_commands |
49 thy_load.base_syntax.thy_load_commands |
46 |
50 |
47 def loaded_theories: Set[String] = |
51 def loaded_theories: Set[String] = |
48 (thy_load.loaded_theories /: rev_deps) { case (loaded, (name, _)) => loaded + name.theory } |
52 (thy_load.loaded_theories /: rev_deps) { case (loaded, (name, _)) => loaded + name.theory } |
49 |
53 |
50 def syntax: Outer_Syntax = |
54 def syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords) |
51 (thy_load.base_syntax /: rev_deps) { case (syn, (name, h)) => |
|
52 val syn1 = syn.add_keywords(h) |
|
53 // FIXME avoid hardwired stuff!? |
|
54 // FIXME broken?! |
|
55 if (name.theory == "Pure") |
|
56 syn1 + |
|
57 ("hence", (Keyword.PRF_ASM_GOAL, Nil), "then have") + |
|
58 ("thus", (Keyword.PRF_ASM_GOAL, Nil), "then show") |
|
59 else syn1 |
|
60 } |
|
61 } |
55 } |
62 |
56 |
63 private def require_thys(initiators: List[Document.Node.Name], |
57 private def require_thys(initiators: List[Document.Node.Name], |
64 required: Dependencies, names: List[Document.Node.Name]): Dependencies = |
58 required: Dependencies, names: List[Document.Node.Name]): Dependencies = |
65 (required /: names)(require_thy(initiators, _, _)) |
59 (required /: names)(require_thy(initiators, _, _)) |