equal
deleted
inserted
replaced
116 def init(session: Session): Unit = {} |
116 def init(session: Session): Unit = {} |
117 def exit(): Unit = {} |
117 def exit(): Unit = {} |
118 def functions: Protocol_Functions = Nil |
118 def functions: Protocol_Functions = Nil |
119 def prover_options(options: Options): Options = options |
119 def prover_options(options: Options): Options = options |
120 } |
120 } |
|
121 |
|
122 |
|
123 /* bootstrap session */ |
|
124 |
|
125 def bootstrap(options: Options): Session = |
|
126 new Session { |
|
127 override def session_options: Options = options |
|
128 override def resources: Resources = Resources.bootstrap |
|
129 } |
121 } |
130 } |
122 |
131 |
123 |
132 |
124 abstract class Session extends Document.Session { |
133 abstract class Session extends Document.Session { |
125 session => |
134 session => |
126 |
135 |
127 def session_options: Options |
136 def session_options: Options |
128 |
137 def resources: Resources |
129 def resources: Resources = Resources.bootstrap |
|
130 |
138 |
131 val store: Store = Store(session_options) |
139 val store: Store = Store(session_options) |
132 def cache: Rich_Text.Cache = store.cache |
140 def cache: Rich_Text.Cache = store.cache |
133 |
141 |
134 def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.empty |
142 def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.empty |