equal
deleted
inserted
replaced
1 /* Title: Pure/System/session.scala |
1 /* Title: Pure/System/session.scala |
2 Author: Makarius |
2 Author: Makarius |
3 Options: :folding=explicit:collapseFolds=1: |
3 Options: :folding=explicit:collapseFolds=1: |
4 |
4 |
5 Isabelle session, potentially with running prover. |
5 Main Isabelle/Scala session, potentially with running prover process. |
6 */ |
6 */ |
7 |
7 |
8 package isabelle |
8 package isabelle |
9 |
9 |
10 import java.lang.System |
10 import java.lang.System |
122 |
122 |
123 |
123 |
124 |
124 |
125 /** main protocol actor **/ |
125 /** main protocol actor **/ |
126 |
126 |
127 val thy_header = new Thy_Header(system.symbols) |
127 /* global state */ |
128 |
128 |
129 @volatile private var syntax = new Outer_Syntax(system.symbols) |
129 @volatile private var syntax = new Outer_Syntax(system.symbols) |
130 def current_syntax(): Outer_Syntax = syntax |
130 def current_syntax(): Outer_Syntax = syntax |
131 |
131 |
132 @volatile private var reverse_syslog = List[XML.Elem]() |
132 @volatile private var reverse_syslog = List[XML.Elem]() |
141 } |
141 } |
142 def is_ready: Boolean = phase == Session.Ready |
142 def is_ready: Boolean = phase == Session.Ready |
143 |
143 |
144 private val global_state = new Volatile(Document.State.init) |
144 private val global_state = new Volatile(Document.State.init) |
145 def current_state(): Document.State = global_state.peek() |
145 def current_state(): Document.State = global_state.peek() |
|
146 |
|
147 |
|
148 /* theory files */ |
|
149 |
|
150 val thy_header = new Thy_Header(system.symbols) |
|
151 |
|
152 val thy_load = new Thy_Load |
|
153 { |
|
154 override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) = |
|
155 { |
|
156 val file = system.platform_file(dir + Thy_Header.thy_path(name)) |
|
157 if (!file.exists || !file.isFile) error("No such file: " + Library.quote(file.toString)) |
|
158 val text = Standard_System.read_file(file) |
|
159 val header = thy_header.read(text) |
|
160 (text, header) |
|
161 } |
|
162 } |
|
163 |
|
164 val thy_info = new Thy_Info(thy_load) |
|
165 |
|
166 |
|
167 /* actor messages */ |
146 |
168 |
147 private case object Interrupt_Prover |
169 private case object Interrupt_Prover |
148 private case class Edit_Node(thy_name: String, |
170 private case class Edit_Node(thy_name: String, |
149 header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit]) |
171 header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit]) |
150 private case class Init_Node(thy_name: String, |
172 private case class Init_Node(thy_name: String, |