equal
deleted
inserted
replaced
14 import scala.actors.Actor._ |
14 import scala.actors.Actor._ |
15 |
15 |
16 |
16 |
17 object Session |
17 object Session |
18 { |
18 { |
|
19 /* abstract file store */ |
|
20 |
|
21 abstract class File_Store |
|
22 { |
|
23 def read(path: Path): String |
|
24 } |
|
25 |
|
26 |
19 /* events */ |
27 /* events */ |
20 |
28 |
21 case object Global_Settings |
29 case object Global_Settings |
22 case object Perspective |
30 case object Perspective |
23 case object Assignment |
31 case object Assignment |
30 case object Ready extends Phase |
38 case object Ready extends Phase |
31 case object Shutdown extends Phase // transient |
39 case object Shutdown extends Phase // transient |
32 } |
40 } |
33 |
41 |
34 |
42 |
35 class Session(val system: Isabelle_System) |
43 class Session(val system: Isabelle_System, val file_store: Session.File_Store) |
36 { |
44 { |
37 /* real time parameters */ // FIXME properties or settings (!?) |
45 /* real time parameters */ // FIXME properties or settings (!?) |
38 |
46 |
39 // user input (e.g. text edits, cursor movement) |
47 // user input (e.g. text edits, cursor movement) |
40 val input_delay = Time.seconds(0.3) |
48 val input_delay = Time.seconds(0.3) |