equal
deleted
inserted
replaced
115 |
115 |
116 /* global state */ |
116 /* global state */ |
117 |
117 |
118 @volatile var loaded_theories: Set[String] = Set() |
118 @volatile var loaded_theories: Set[String] = Set() |
119 |
119 |
120 @volatile private var syntax = new Outer_Syntax(Isabelle_System.symbols) |
120 @volatile private var syntax = new Outer_Syntax |
121 def current_syntax(): Outer_Syntax = syntax |
121 def current_syntax(): Outer_Syntax = syntax |
122 |
122 |
123 @volatile private var reverse_syslog = List[XML.Elem]() |
123 @volatile private var reverse_syslog = List[XML.Elem]() |
124 def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n") |
124 def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n") |
125 |
125 |
200 c2 match { |
200 c2 match { |
201 case None => None |
201 case None => None |
202 case Some(command) => |
202 case Some(command) => |
203 if (global_state.peek().lookup_command(command.id).isEmpty) { |
203 if (global_state.peek().lookup_command(command.id).isEmpty) { |
204 global_state.change(_.define_command(command)) |
204 global_state.change(_.define_command(command)) |
205 prover.get. |
205 prover.get.define_command(command.id, Symbol.encode(command.source)) |
206 define_command(command.id, |
|
207 Isabelle_System.symbols.encode(command.source)) |
|
208 } |
206 } |
209 Some(command.id) |
207 Some(command.id) |
210 } |
208 } |
211 (id1, id2) |
209 (id1, id2) |
212 } |
210 } |