equal
deleted
inserted
replaced
73 val cache: Term.Cache = Term.Cache.make() |
73 val cache: Term.Cache = Term.Cache.make() |
74 |
74 |
75 private val theory_cache = Synchronized(Map.empty[String, Export_Theory.Theory]) |
75 private val theory_cache = Synchronized(Map.empty[String, Export_Theory.Theory]) |
76 def cache_theory(thy_name: String, make_thy: => Export_Theory.Theory): Export_Theory.Theory = |
76 def cache_theory(thy_name: String, make_thy: => Export_Theory.Theory): Export_Theory.Theory = |
77 { |
77 { |
78 theory_cache.change_result(thys => |
78 theory_cache.value.get(thy_name) match { |
79 { |
79 case Some(thy) => thy |
80 thys.get(thy_name) match { |
80 case None => |
81 case Some(thy) => (thy, thys) |
81 val thy1 = make_thy |
82 case None => |
82 theory_cache.change_result(thys => |
83 val thy = make_thy |
83 { |
84 (thy, thys + (thy_name -> thy)) |
84 thys.get(thy_name) match { |
85 } |
85 case Some(thy) => (thy, thys) |
86 }) |
86 case None => (thy1, thys + (thy_name -> thy1)) |
|
87 } |
|
88 }) |
|
89 } |
87 } |
90 } |
88 } |
91 } |
89 |
92 |
90 |
93 |
91 /* presentation elements */ |
94 /* presentation elements */ |