7 */ |
7 */ |
8 |
8 |
9 package isabelle.prover |
9 package isabelle.prover |
10 |
10 |
11 |
11 |
12 import scala.collection.mutable.{HashMap, HashSet} |
12 import scala.collection.mutable |
13 import scala.collection.immutable.{TreeSet} |
13 import scala.collection.immutable.{TreeSet} |
14 |
14 |
15 import org.gjt.sp.util.Log |
15 import org.gjt.sp.util.Log |
16 |
16 |
17 import isabelle.proofdocument.{ProofDocument, Text, Token} |
17 import isabelle.proofdocument.{ProofDocument, Text, Token} |
21 class Prover(isabelle_system: IsabelleSystem) |
21 class Prover(isabelle_system: IsabelleSystem) |
22 { |
22 { |
23 private var _logic = isabelle_system.getenv_strict("ISABELLE_LOGIC") |
23 private var _logic = isabelle_system.getenv_strict("ISABELLE_LOGIC") |
24 private var process: Isar = null |
24 private var process: Isar = null |
25 |
25 |
26 private val commands = new HashMap[IsarDocument.Command_ID, Command] |
26 private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command] |
27 |
27 |
28 |
28 |
29 /* outer syntax keywords */ |
29 /* outer syntax keywords */ |
30 |
30 |
31 val decl_info = new EventBus[(String, String)] |
31 val decl_info = new EventBus[(String, String)] |
32 |
32 |
33 private val keyword_decls = new HashSet[String] { |
33 private val keyword_decls = new mutable.HashSet[String] { |
34 override def +=(name: String) = { |
34 override def +=(name: String) = { |
35 decl_info.event(name, OuterKeyword.MINOR) |
35 decl_info.event(name, OuterKeyword.MINOR) |
36 super.+=(name) |
36 super.+=(name) |
37 } |
37 } |
38 } |
38 } |
39 private val command_decls = new HashMap[String, String] { |
39 private val command_decls = new mutable.HashMap[String, String] { |
40 override def +=(entry: (String, String)) = { |
40 override def +=(entry: (String, String)) = { |
41 decl_info.event(entry) |
41 decl_info.event(entry) |
42 super.+=(entry) |
42 super.+=(entry) |
43 } |
43 } |
44 } |
44 } |