1/* Title: Pure/Thy/thy_resources.scala 2 Author: Makarius 3 4PIDE resources for theory files: load/unload theories via PIDE document updates. 5*/ 6 7package isabelle 8 9 10import java.io.{File => JFile} 11 12 13object Thy_Resources 14{ 15 /* PIDE session */ 16 17 def start_session( 18 options: Options, 19 session_name: String, 20 session_dirs: List[Path] = Nil, 21 include_sessions: List[String] = Nil, 22 session_base: Option[Sessions.Base] = None, 23 print_mode: List[String] = Nil, 24 progress: Progress = No_Progress, 25 log: Logger = No_Logger): Session = 26 { 27 val base = 28 session_base getOrElse 29 Sessions.base_info(options, session_name, include_sessions = include_sessions, 30 progress = progress, dirs = session_dirs).check_base 31 val resources = new Thy_Resources(base, log = log) 32 val session = new Session(session_name, options, resources) 33 34 val session_error = Future.promise[String] 35 var session_phase: Session.Consumer[Session.Phase] = null 36 session_phase = 37 Session.Consumer(getClass.getName) { 38 case Session.Ready => 39 session.phase_changed -= session_phase 40 session_error.fulfill("") 41 case Session.Terminated(result) if !result.ok => 42 session.phase_changed -= session_phase 43 session_error.fulfill("Session start failed: return code " + result.rc) 44 case _ => 45 } 46 session.phase_changed += session_phase 47 48 progress.echo("Starting " + session_name + " ...") 49 Isabelle_Process.start(session, options, 50 logic = session_name, dirs = session_dirs, modes = print_mode) 51 52 session_error.join match { 53 case "" => session 54 case msg => session.stop(); error(msg) 55 } 56 } 57 58 class Theories_Result private[Thy_Resources]( 59 val state: Document.State, 60 val version: Document.Version, 61 val nodes: List[(Document.Node.Name, Protocol.Node_Status)]) 62 { 63 def node_names: List[Document.Node.Name] = nodes.map(_._1) 64 def ok: Boolean = nodes.forall({ case (_, st) => st.ok }) 65 66 def snapshot(node_name: Document.Node.Name): Document.Snapshot = 67 { 68 val snapshot = state.snapshot(node_name) 69 assert(version.id == snapshot.version.id) 70 snapshot 71 } 72 } 73 74 val default_use_theories_check_delay: Double = 0.5 75 76 77 class Session private[Thy_Resources]( 78 session_name: String, 79 session_options: Options, 80 override val resources: Thy_Resources) extends isabelle.Session(session_options, resources) 81 { 82 session => 83 84 val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session") 85 val tmp_dir_name: String = File.path(tmp_dir).implode 86 87 override def toString: String = session_name 88 89 override def stop(): Process_Result = 90 { 91 try { super.stop() } 92 finally { Isabelle_System.rm_tree(tmp_dir) } 93 } 94 95 96 /* theories */ 97 98 def use_theories( 99 theories: List[String], 100 qualifier: String = Sessions.DRAFT, 101 master_dir: String = "", 102 check_delay: Time = Time.seconds(default_use_theories_check_delay), 103 check_limit: Int = 0, 104 id: UUID = UUID(), 105 progress: Progress = No_Progress): Theories_Result = 106 { 107 val dep_theories = 108 resources.load_theories(session, id, theories, qualifier = qualifier, 109 master_dir = proper_string(master_dir) getOrElse tmp_dir_name, progress = progress) 110 111 val result = Future.promise[Theories_Result] 112 113 def check_state(beyond_limit: Boolean = false) 114 { 115 val state = session.current_state() 116 state.stable_tip_version match { 117 case Some(version) => 118 if (beyond_limit || dep_theories.forall(state.node_consolidated(version, _))) { 119 val nodes = 120 for (name <- dep_theories) 121 yield (name -> Protocol.node_status(state, version, name)) 122 try { result.fulfill(new Theories_Result(state, version, nodes)) } 123 catch { case _: IllegalStateException => } 124 } 125 case None => 126 } 127 } 128 129 val check_progress = 130 { 131 var check_count = 0 132 Event_Timer.request(Time.now(), repeat = Some(check_delay)) 133 { 134 if (progress.stopped) result.cancel 135 else { 136 check_count += 1 137 check_state(check_limit > 0 && check_count > check_limit) 138 } 139 } 140 } 141 142 val theories_progress = Synchronized(Set.empty[Document.Node.Name]) 143 144 val consumer = 145 Session.Consumer[Session.Commands_Changed](getClass.getName) { 146 case changed => 147 if (dep_theories.exists(changed.nodes)) { 148 149 val check_theories = 150 (for (command <- changed.commands.iterator if command.potentially_initialized) 151 yield command.node_name).toSet 152 153 if (check_theories.nonEmpty) { 154 val snapshot = session.snapshot() 155 val initialized = 156 theories_progress.change_result(theories => 157 { 158 val initialized = 159 (check_theories -- theories).toList.filter(name => 160 Protocol.node_status(snapshot.state, snapshot.version, name).initialized) 161 (initialized, theories ++ initialized) 162 }) 163 initialized.map(_.theory).sorted.foreach(progress.theory("", _)) 164 } 165 166 check_state() 167 } 168 } 169 170 try { 171 session.commands_changed += consumer 172 result.join_result 173 check_progress.cancel 174 session.commands_changed -= consumer 175 } 176 finally { 177 resources.unload_theories(session, id, dep_theories) 178 } 179 180 result.join 181 } 182 183 def purge_theories( 184 theories: List[String], 185 qualifier: String = Sessions.DRAFT, 186 master_dir: String = "", 187 all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) = 188 resources.purge_theories(session, theories = theories, qualifier = qualifier, 189 master_dir = proper_string(master_dir) getOrElse tmp_dir_name, all = all) 190 } 191 192 193 /* internal state */ 194 195 sealed case class State( 196 required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty, 197 theories: Map[Document.Node.Name, Theory] = Map.empty) 198 { 199 def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name) 200 201 def insert_required(id: UUID, names: List[Document.Node.Name]): State = 202 copy(required = (required /: names)(_.insert(_, id))) 203 204 def remove_required(id: UUID, names: List[Document.Node.Name]): State = 205 copy(required = (required /: names)(_.remove(_, id))) 206 207 def update_theories(update: List[(Document.Node.Name, Theory)]): State = 208 copy(theories = 209 (theories /: update)({ case (thys, (name, thy)) => 210 thys.get(name) match { 211 case Some(thy1) if thy1 == thy => thys 212 case _ => thys + (name -> thy) 213 } 214 })) 215 216 def remove_theories(remove: List[Document.Node.Name]): State = 217 { 218 require(remove.forall(name => !is_required(name))) 219 copy(theories = theories -- remove) 220 } 221 222 lazy val theories_graph: Graph[Document.Node.Name, Unit] = 223 { 224 val entries = 225 for ((name, theory) <- theories.toList) 226 yield ((name, ()), theory.node_header.imports.map(_._1).filter(theories.isDefinedAt(_))) 227 Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering) 228 } 229 } 230 231 final class Theory private[Thy_Resources]( 232 val node_name: Document.Node.Name, 233 val node_header: Document.Node.Header, 234 val text: String, 235 val node_required: Boolean) 236 { 237 override def toString: String = node_name.toString 238 239 def node_perspective: Document.Node.Perspective_Text = 240 Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty) 241 242 def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] = 243 List(node_name -> Document.Node.Deps(node_header), 244 node_name -> Document.Node.Edits(text_edits), 245 node_name -> node_perspective) 246 247 def node_edits(old: Option[Theory]): List[Document.Edit_Text] = 248 { 249 val (text_edits, old_required) = 250 if (old.isEmpty) (Text.Edit.inserts(0, text), false) 251 else (Text.Edit.replace(0, old.get.text, text), old.get.node_required) 252 253 if (text_edits.isEmpty && node_required == old_required) Nil 254 else make_edits(text_edits) 255 } 256 257 def purge_edits: List[Document.Edit_Text] = 258 make_edits(Text.Edit.removes(0, text)) 259 260 def required(required: Boolean): Theory = 261 if (required == node_required) this 262 else new Theory(node_name, node_header, text, required) 263 } 264} 265 266class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger) 267 extends Resources(session_base, log = log) 268{ 269 resources => 270 271 private val state = Synchronized(Thy_Resources.State()) 272 273 def load_theories( 274 session: Session, 275 id: UUID, 276 theories: List[String], 277 qualifier: String, 278 master_dir: String, 279 progress: Progress): List[Document.Node.Name] = 280 { 281 val import_names = theories.map(thy => import_name(qualifier, master_dir, thy) -> Position.none) 282 val dependencies = resources.dependencies(import_names, progress = progress).check_errors 283 val dep_theories = dependencies.theories 284 285 val loaded_theories = 286 for (node_name <- dep_theories) 287 yield { 288 val path = node_name.path 289 if (!node_name.is_theory) error("Not a theory file: " + path) 290 291 progress.expose_interrupt() 292 val text = File.read(path) 293 val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text)) 294 new Thy_Resources.Theory(node_name, node_header, text, true) 295 } 296 297 state.change(st => 298 { 299 val st1 = st.insert_required(id, dep_theories) 300 val theory_edits = 301 for (theory <- loaded_theories) 302 yield { 303 val node_name = theory.node_name 304 val theory1 = theory.required(st1.is_required(node_name)) 305 val edits = theory1.node_edits(st1.theories.get(node_name)) 306 (edits, (node_name, theory1)) 307 } 308 session.update(Document.Blobs.empty, theory_edits.flatMap(_._1)) 309 st1.update_theories(theory_edits.map(_._2)) 310 }) 311 312 dep_theories 313 } 314 315 def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name]) 316 { 317 state.change(st => 318 { 319 val st1 = st.remove_required(id, dep_theories) 320 val theory_edits = 321 for { 322 node_name <- dep_theories 323 theory <- st1.theories.get(node_name) 324 } 325 yield { 326 val theory1 = theory.required(st1.is_required(node_name)) 327 val edits = theory1.node_edits(Some(theory)) 328 (edits, (node_name, theory1)) 329 } 330 session.update(Document.Blobs.empty, theory_edits.flatMap(_._1)) 331 st1.update_theories(theory_edits.map(_._2)) 332 }) 333 } 334 335 def purge_theories(session: Session, 336 theories: List[String], 337 qualifier: String, 338 master_dir: String, 339 all: Boolean): (List[Document.Node.Name], List[Document.Node.Name]) = 340 { 341 val nodes = theories.map(import_name(qualifier, master_dir, _)) 342 343 state.change_result(st => 344 { 345 val graph = st.theories_graph 346 val all_nodes = graph.topological_order 347 348 val purge = 349 (if (all) all_nodes else nodes.filter(graph.defined(_))). 350 filterNot(st.is_required(_)).toSet 351 352 val retain = graph.all_preds(all_nodes.filterNot(purge)).toSet 353 val (retained, purged) = all_nodes.partition(retain) 354 355 val purge_edits = purged.flatMap(name => st.theories(name).purge_edits) 356 session.update(Document.Blobs.empty, purge_edits) 357 358 ((purged, retained), st.remove_theories(purged)) 359 }) 360 } 361} 362