src/Pure/Thy/sessions.scala
changeset 66770 122df1fde073
parent 66764 006deaf5c3dc
child 66780 bf54ca580bf2
equal deleted inserted replaced
66769:97f16ada519c 66770:122df1fde073
   129     def loaded_theory_syntax(name: String): Option[Outer_Syntax] =
   129     def loaded_theory_syntax(name: String): Option[Outer_Syntax] =
   130       if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None
   130       if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None
   131     def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] =
   131     def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] =
   132       loaded_theory_syntax(name.theory)
   132       loaded_theory_syntax(name.theory)
   133 
   133 
   134     def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Option[Outer_Syntax] =
   134     def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax =
   135       nodes(name).syntax orElse loaded_theory_syntax(name)
   135       nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
   136 
   136 
   137     def known_theory(name: String): Option[Document.Node.Name] =
   137     def known_theory(name: String): Option[Document.Node.Name] =
   138       known.theories.get(name)
   138       known.theories.get(name)
   139 
   139 
   140     def dest_known_theories: List[(String, String)] =
   140     def dest_known_theories: List[(String, String)] =