equal
deleted
inserted
replaced
109 class Engine(val name: String) extends Isabelle_System.Service { |
109 class Engine(val name: String) extends Isabelle_System.Service { |
110 override def toString: String = name |
110 override def toString: String = name |
111 |
111 |
112 def build_options(options: Options, build_cluster: Boolean = false): Options = { |
112 def build_options(options: Options, build_cluster: Boolean = false): Options = { |
113 val options1 = options + "completion_limit=0" + "editor_tracing_messages=0" |
113 val options1 = options + "completion_limit=0" + "editor_tracing_messages=0" |
114 if (build_cluster) options1 + "build_database_server" + "build_database" |
114 if (build_cluster) options1 + "build_database_server" + "build_database" else options1 |
115 else options1 |
|
116 } |
115 } |
117 |
116 |
118 final def build_store(options: Options, |
117 final def build_store(options: Options, |
119 build_cluster: Boolean = false, |
118 build_cluster: Boolean = false, |
120 cache: Term.Cache = Term.Cache.make() |
119 cache: Term.Cache = Term.Cache.make() |