equal
deleted
inserted
replaced
65 } |
65 } |
66 catch { |
66 catch { |
67 case e: IOException => |
67 case e: IOException => |
68 } |
68 } |
69 } |
69 } |
|
70 |
|
71 |
|
72 /* unique ids */ // FIXME specific to "session" (!??) |
|
73 |
|
74 private var id_count: BigInt = 0 |
|
75 def id() : String = synchronized { id_count += 1; "editor:" + id_count } |
70 |
76 |
71 |
77 |
72 // mapping buffer <-> prover |
78 // mapping buffer <-> prover |
73 |
79 |
74 private val mapping = new HashMap[JEditBuffer, ProverSetup] |
80 private val mapping = new HashMap[JEditBuffer, ProverSetup] |