equal
deleted
inserted
replaced
8 signature BASIC_OUTER_SYNTAX = |
8 signature BASIC_OUTER_SYNTAX = |
9 sig |
9 sig |
10 structure Isar: |
10 structure Isar: |
11 sig |
11 sig |
12 val state: unit -> Toplevel.state |
12 val state: unit -> Toplevel.state |
|
13 val context: unit -> Proof.context |
13 val exn: unit -> (exn * string) option |
14 val exn: unit -> (exn * string) option |
14 val main: unit -> unit |
15 val main: unit -> unit |
15 val loop: unit -> unit |
16 val loop: unit -> unit |
16 val sync_main: unit -> unit |
17 val sync_main: unit -> unit |
17 val sync_loop: unit -> unit |
18 val sync_loop: unit -> unit |
321 gen_loop term no_pos); |
322 gen_loop term no_pos); |
322 |
323 |
323 structure Isar = |
324 structure Isar = |
324 struct |
325 struct |
325 val state = Toplevel.get_state; |
326 val state = Toplevel.get_state; |
|
327 val context = Context.proof_of o Toplevel.context_of o state; |
326 val exn = Toplevel.exn; |
328 val exn = Toplevel.exn; |
327 fun main () = gen_main false false; |
329 fun main () = gen_main false false; |
328 fun loop () = gen_loop false false; |
330 fun loop () = gen_loop false false; |
329 fun sync_main () = gen_main true true; |
331 fun sync_main () = gen_main true true; |
330 fun sync_loop () = gen_loop true true; |
332 fun sync_loop () = gen_loop true true; |