equal
deleted
inserted
replaced
130 def loaded_theory_syntax(name: String): Option[Outer_Syntax] = |
130 def loaded_theory_syntax(name: String): Option[Outer_Syntax] = |
131 if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None |
131 if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None |
132 def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] = |
132 def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] = |
133 loaded_theory_syntax(name.theory) |
133 loaded_theory_syntax(name.theory) |
134 |
134 |
|
135 def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Option[Outer_Syntax] = |
|
136 nodes(name).syntax orElse loaded_theory_syntax(name) |
|
137 |
135 def known_theory(name: String): Option[Document.Node.Name] = |
138 def known_theory(name: String): Option[Document.Node.Name] = |
136 known.theories.get(name) |
139 known.theories.get(name) |
137 |
140 |
138 def dest_known_theories: List[(String, String)] = |
141 def dest_known_theories: List[(String, String)] = |
139 for ((theory, node_name) <- known.theories.toList) |
142 for ((theory, node_name) <- known.theories.toList) |