1/* Title: Tools/jEdit/src/document_model.scala 2 Author: Fabian Immler, TU Munich 3 Author: Makarius 4 5Document model connected to jEdit buffer or external file: content of theory 6node or auxiliary file (blob). 7*/ 8 9package isabelle.jedit 10 11 12import isabelle._ 13 14import java.io.{File => JFile} 15 16import scala.collection.mutable 17import scala.annotation.tailrec 18 19import org.gjt.sp.jedit.{jEdit, View} 20import org.gjt.sp.jedit.Buffer 21import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} 22 23 24object Document_Model 25{ 26 /* document models */ 27 28 sealed case class State( 29 models: Map[Document.Node.Name, Document_Model] = Map.empty, 30 buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty, 31 overlays: Document.Overlays = Document.Overlays.empty) 32 { 33 def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] = 34 for { 35 (node_name, model) <- models.iterator 36 if model.isInstanceOf[File_Model] 37 } yield (node_name, model.asInstanceOf[File_Model]) 38 39 def document_blobs: Document.Blobs = 40 Document.Blobs( 41 (for { 42 (node_name, model) <- models.iterator 43 blob <- model.get_blob 44 } yield (node_name -> blob)).toMap) 45 46 def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer) 47 : (Buffer_Model, State) = 48 { 49 val old_model = 50 models.get(node_name) match { 51 case Some(file_model: File_Model) => Some(file_model) 52 case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit()) 53 case _ => None 54 } 55 val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model) 56 (buffer_model, 57 copy(models = models + (node_name -> buffer_model), 58 buffer_models = buffer_models + (buffer -> buffer_model))) 59 } 60 61 def close_buffer(buffer: JEditBuffer): State = 62 { 63 buffer_models.get(buffer) match { 64 case None => this 65 case Some(buffer_model) => 66 val file_model = buffer_model.exit() 67 copy(models = models + (file_model.node_name -> file_model), 68 buffer_models = buffer_models - buffer) 69 } 70 } 71 72 def provide_file(session: Session, node_name: Document.Node.Name, text: String): State = 73 if (models.isDefinedAt(node_name)) this 74 else { 75 val edit = Text.Edit.insert(0, text) 76 val model = File_Model.init(session, node_name, text, pending_edits = List(edit)) 77 copy(models = models + (node_name -> model)) 78 } 79 } 80 81 private val state = Synchronized(State()) // owned by GUI thread 82 83 def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models 84 def get(name: Document.Node.Name): Option[Document_Model] = get_models.get(name) 85 def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer) 86 87 def document_blobs(): Document.Blobs = state.value.document_blobs 88 89 90 /* bibtex */ 91 92 def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] = 93 Bibtex.entries_iterator(state.value.models) 94 95 def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset) 96 : Option[Completion.Result] = 97 Bibtex.completion(history, rendering, caret, state.value.models) 98 99 100 /* overlays */ 101 102 def node_overlays(name: Document.Node.Name): Document.Node.Overlays = 103 state.value.overlays(name) 104 105 def insert_overlay(command: Command, fn: String, args: List[String]): Unit = 106 state.change(st => st.copy(overlays = st.overlays.insert(command, fn, args))) 107 108 def remove_overlay(command: Command, fn: String, args: List[String]): Unit = 109 state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args))) 110 111 112 /* sync external files */ 113 114 def sync_files(changed_files: Set[JFile]): Boolean = 115 { 116 state.change_result(st => 117 { 118 val changed_models = 119 (for { 120 (node_name, model) <- st.file_models_iterator 121 file <- model.file if changed_files(file) 122 text <- PIDE.resources.read_file_content(node_name) 123 if model.content.text != text 124 } yield { 125 val content = Document_Model.File_Content(text) 126 val edits = Text.Edit.replace(0, model.content.text, text) 127 (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits)) 128 }).toList 129 if (changed_models.isEmpty) (false, st) 130 else (true, st.copy(models = (st.models /: changed_models)(_ + _))) 131 }) 132 } 133 134 135 /* syntax */ 136 137 def syntax_changed(names: List[Document.Node.Name]) 138 { 139 GUI_Thread.require {} 140 141 val models = state.value.models 142 for (name <- names.iterator; model <- models.get(name)) { 143 model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => } 144 } 145 } 146 147 148 /* init and exit */ 149 150 def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model = 151 { 152 GUI_Thread.require {} 153 state.change_result(st => 154 st.buffer_models.get(buffer) match { 155 case Some(buffer_model) if buffer_model.node_name == node_name => 156 buffer_model.init_token_marker 157 (buffer_model, st) 158 case _ => 159 val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer) 160 buffer.propertiesChanged 161 res 162 }) 163 } 164 165 def exit(buffer: Buffer) 166 { 167 GUI_Thread.require {} 168 state.change(st => 169 if (st.buffer_models.isDefinedAt(buffer)) { 170 val res = st.close_buffer(buffer) 171 buffer.propertiesChanged 172 res 173 } 174 else st) 175 } 176 177 def provide_files(session: Session, files: List[(Document.Node.Name, String)]) 178 { 179 GUI_Thread.require {} 180 state.change(st => 181 (st /: files) { case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) }) 182 } 183 184 185 /* required nodes */ 186 187 def required_nodes(): Set[Document.Node.Name] = 188 (for { 189 (node_name, model) <- state.value.models.iterator 190 if model.node_required 191 } yield node_name).toSet 192 193 def node_required(name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false) 194 { 195 GUI_Thread.require {} 196 197 val changed = 198 state.change_result(st => 199 st.models.get(name) match { 200 case None => (false, st) 201 case Some(model) => 202 val required = if (toggle) !model.node_required else set 203 model match { 204 case model1: File_Model if required != model1.node_required => 205 (true, st.copy(models = st.models + (name -> model1.copy(node_required = required)))) 206 case model1: Buffer_Model if required != model1.node_required => 207 model1.set_node_required(required); (true, st) 208 case _ => (false, st) 209 } 210 }) 211 if (changed) { 212 PIDE.plugin.options_changed() 213 PIDE.editor.flush() 214 } 215 } 216 217 def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit = 218 Document_Model.get(view.getBuffer).foreach(model => 219 node_required(model.node_name, toggle = toggle, set = set)) 220 221 222 /* flushed edits */ 223 224 def flush_edits(hidden: Boolean, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) = 225 { 226 GUI_Thread.require {} 227 228 state.change_result(st => 229 { 230 val doc_blobs = st.document_blobs 231 232 val buffer_edits = 233 (for { 234 (_, model) <- st.buffer_models.iterator 235 edit <- model.flush_edits(doc_blobs, hidden).iterator 236 } yield edit).toList 237 238 val file_edits = 239 (for { 240 (node_name, model) <- st.file_models_iterator 241 (edits, model1) <- model.flush_edits(doc_blobs, hidden) 242 } yield (edits, node_name -> model1)).toList 243 244 val model_edits = buffer_edits ::: file_edits.flatMap(_._1) 245 246 val purge_edits = 247 if (purge) { 248 val purged = 249 (for ((node_name, model) <- st.file_models_iterator) 250 yield (node_name -> model.purge_edits(doc_blobs))).toList 251 252 val imports = 253 { 254 val open_nodes = 255 (for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList 256 val touched_nodes = model_edits.map(_._1) 257 val pending_nodes = for ((node_name, None) <- purged) yield node_name 258 (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none)) 259 } 260 val retain = PIDE.resources.dependencies(imports).theories.toSet 261 262 for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits) 263 yield edit 264 } 265 else Nil 266 267 val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1)) 268 PIDE.plugin.file_watcher.purge( 269 (for { 270 (_, model) <- st1.file_models_iterator 271 file <- model.file 272 } yield file.getParentFile).toSet) 273 274 ((doc_blobs, model_edits ::: purge_edits), st1) 275 }) 276 } 277 278 279 /* file content */ 280 281 sealed case class File_Content(text: String) 282 { 283 lazy val bytes: Bytes = Bytes(Symbol.encode(text)) 284 lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) 285 lazy val bibtex_entries: List[Text.Info[String]] = 286 try { Bibtex.entries(text) } 287 catch { case ERROR(_) => Nil } 288 } 289 290 291 /* HTTP preview */ 292 293 private val plain_text_prefix = "plain_text=" 294 295 def open_preview(view: View, plain_text: Boolean) 296 { 297 Document_Model.get(view.getBuffer) match { 298 case Some(model) => 299 val name = model.node_name 300 val url = 301 PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview?" + 302 (if (plain_text) plain_text_prefix else "") + Url.encode(name.node) 303 PIDE.editor.hyperlink_url(url).follow(view) 304 case _ => 305 } 306 } 307 308 def http_handlers(http_root: String): List[HTTP.Handler] = 309 { 310 val fonts_root = http_root + "/fonts" 311 val preview_root = http_root + "/preview" 312 313 val preview = 314 HTTP.get(preview_root, arg => 315 for { 316 query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode(_)) 317 name = Library.perhaps_unprefix(plain_text_prefix, query) 318 model <- get(PIDE.resources.node_name(name)) 319 } 320 yield { 321 val snapshot = model.await_stable_snapshot() 322 val preview = 323 Present.preview(snapshot, fonts_url = HTML.fonts_dir(fonts_root), 324 plain_text = query.startsWith(plain_text_prefix)) 325 HTTP.Response.html(preview.content) 326 }) 327 328 List(HTTP.fonts(fonts_root), preview) 329 } 330} 331 332sealed abstract class Document_Model extends Document.Model 333{ 334 /* perspective */ 335 336 def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil 337 338 def node_perspective( 339 doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) = 340 { 341 GUI_Thread.require {} 342 343 if (Isabelle.continuous_checking && is_theory) { 344 val snapshot = this.snapshot() 345 346 val reparse = snapshot.node.load_commands_changed(doc_blobs) 347 val perspective = 348 if (hidden) Text.Perspective.empty 349 else { 350 val view_ranges = document_view_ranges(snapshot) 351 val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_)) 352 Text.Perspective(view_ranges ::: load_ranges) 353 } 354 val overlays = PIDE.editor.node_overlays(node_name) 355 356 (reparse, Document.Node.Perspective(node_required, perspective, overlays)) 357 } 358 else (false, Document.Node.no_perspective_text) 359 } 360 361 362 /* snapshot */ 363 364 @tailrec final def await_stable_snapshot(): Document.Snapshot = 365 { 366 val snapshot = this.snapshot() 367 if (snapshot.is_outdated) { 368 Thread.sleep(PIDE.options.seconds("editor_output_delay").ms) 369 await_stable_snapshot() 370 } 371 else snapshot 372 } 373} 374 375object File_Model 376{ 377 def empty(session: Session): File_Model = 378 File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""), 379 false, Document.Node.no_perspective_text, Nil) 380 381 def init(session: Session, 382 node_name: Document.Node.Name, 383 text: String, 384 node_required: Boolean = false, 385 last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, 386 pending_edits: List[Text.Edit] = Nil): File_Model = 387 { 388 val file = JEdit_Lib.check_file(node_name.node) 389 file.foreach(PIDE.plugin.file_watcher.register_parent(_)) 390 391 val content = Document_Model.File_Content(text) 392 val node_required1 = node_required || node_name.is_bibtex_theory 393 File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits) 394 } 395} 396 397case class File_Model( 398 session: Session, 399 node_name: Document.Node.Name, 400 file: Option[JFile], 401 content: Document_Model.File_Content, 402 node_required: Boolean, 403 last_perspective: Document.Node.Perspective_Text, 404 pending_edits: List[Text.Edit]) extends Document_Model 405{ 406 /* text */ 407 408 def get_text(range: Text.Range): Option[String] = 409 range.try_substring(content.text) 410 411 412 /* header */ 413 414 def node_header: Document.Node.Header = 415 PIDE.resources.special_header(node_name) getOrElse 416 PIDE.resources.check_thy_reader(node_name, Scan.char_reader(content.text), strict = false) 417 418 419 /* content */ 420 421 def node_position(offset: Text.Offset): Line.Node_Position = 422 Line.Node_Position(node_name.node, 423 Line.Position.zero.advance(content.text.substring(0, offset))) 424 425 def get_blob: Option[Document.Blob] = 426 if (is_theory) None 427 else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)) 428 429 def bibtex_entries: List[Text.Info[String]] = 430 if (is_bibtex) content.bibtex_entries else Nil 431 432 433 /* edits */ 434 435 def update_text(text: String): Option[File_Model] = 436 Text.Edit.replace(0, content.text, text) match { 437 case Nil => None 438 case edits => 439 val content1 = Document_Model.File_Content(text) 440 val pending_edits1 = pending_edits ::: edits 441 Some(copy(content = content1, pending_edits = pending_edits1)) 442 } 443 444 def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean) 445 : Option[(List[Document.Edit_Text], File_Model)] = 446 { 447 val (reparse, perspective) = node_perspective(doc_blobs, hidden) 448 if (reparse || pending_edits.nonEmpty || last_perspective != perspective) { 449 val edits = node_edits(node_header, pending_edits, perspective) 450 Some((edits, copy(last_perspective = perspective, pending_edits = Nil))) 451 } 452 else None 453 } 454 455 def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] = 456 if (pending_edits.nonEmpty || 457 !is_bibtex_theory && 458 (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None 459 else { 460 val text_edits = List(Text.Edit.remove(0, content.text)) 461 Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text)) 462 } 463 464 465 /* snapshot */ 466 467 def is_stable: Boolean = pending_edits.isEmpty 468 def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) 469} 470 471case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer) 472 extends Document_Model 473{ 474 /* text */ 475 476 def get_text(range: Text.Range): Option[String] = 477 JEdit_Lib.get_text(buffer, range) 478 479 480 /* header */ 481 482 def node_header(): Document.Node.Header = 483 { 484 GUI_Thread.require {} 485 486 PIDE.resources.special_header(node_name) getOrElse 487 JEdit_Lib.buffer_lock(buffer) { 488 PIDE.resources.check_thy_reader(node_name, JEdit_Lib.buffer_reader(buffer), strict = false) 489 } 490 } 491 492 493 /* perspective */ 494 495 // owned by GUI thread 496 private var _node_required = false 497 def node_required: Boolean = _node_required 498 def set_node_required(b: Boolean) { GUI_Thread.require { _node_required = b } } 499 500 def document_view_iterator: Iterator[Document_View] = 501 for { 502 text_area <- JEdit_Lib.jedit_text_areas(buffer) 503 doc_view <- Document_View.get(text_area) 504 } yield doc_view 505 506 override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = 507 { 508 GUI_Thread.require {} 509 510 (for { 511 doc_view <- document_view_iterator 512 range <- doc_view.perspective(snapshot).ranges.iterator 513 } yield range).toList 514 } 515 516 517 /* blob */ 518 519 // owned by GUI thread 520 private var _blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None 521 522 private def reset_blob(): Unit = GUI_Thread.require { _blob = None } 523 524 def get_blob: Option[Document.Blob] = 525 GUI_Thread.require { 526 if (is_theory) None 527 else { 528 val (bytes, text, chunk) = 529 _blob match { 530 case Some(x) => x 531 case None => 532 val bytes = PIDE.resources.make_file_content(buffer) 533 val text = buffer.getText(0, buffer.getLength) 534 val chunk = Symbol.Text_Chunk(text) 535 val x = (bytes, text, chunk) 536 _blob = Some(x) 537 x 538 } 539 val changed = pending_edits.nonEmpty 540 Some(Document.Blob(bytes, text, chunk, changed)) 541 } 542 } 543 544 545 /* bibtex entries */ 546 547 // owned by GUI thread 548 private var _bibtex_entries: Option[List[Text.Info[String]]] = None 549 550 private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None } 551 552 def bibtex_entries: List[Text.Info[String]] = 553 GUI_Thread.require { 554 if (is_bibtex) { 555 _bibtex_entries match { 556 case Some(entries) => entries 557 case None => 558 val text = JEdit_Lib.buffer_text(buffer) 559 val entries = 560 try { Bibtex.entries(text) } 561 catch { case ERROR(msg) => Output.warning(msg); Nil } 562 _bibtex_entries = Some(entries) 563 entries 564 } 565 } 566 else Nil 567 } 568 569 570 /* pending edits */ 571 572 private object pending_edits 573 { 574 private val pending = new mutable.ListBuffer[Text.Edit] 575 private var last_perspective = Document.Node.no_perspective_text 576 577 def nonEmpty: Boolean = synchronized { pending.nonEmpty } 578 def get_edits: List[Text.Edit] = synchronized { pending.toList } 579 def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective } 580 def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit = 581 synchronized { last_perspective = perspective } 582 583 def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] = 584 synchronized { 585 GUI_Thread.require {} 586 587 val edits = get_edits 588 val (reparse, perspective) = node_perspective(doc_blobs, hidden) 589 if (reparse || edits.nonEmpty || last_perspective != perspective) { 590 pending.clear 591 last_perspective = perspective 592 node_edits(node_header, edits, perspective) 593 } 594 else Nil 595 } 596 597 def edit(edits: List[Text.Edit]): Unit = synchronized 598 { 599 GUI_Thread.require {} 600 601 reset_blob() 602 reset_bibtex_entries() 603 604 for (doc_view <- document_view_iterator) 605 doc_view.rich_text_area.active_reset() 606 607 pending ++= edits 608 PIDE.editor.invoke() 609 } 610 } 611 612 def is_stable: Boolean = !pending_edits.nonEmpty 613 def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits) 614 615 def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] = 616 pending_edits.flush_edits(doc_blobs, hidden) 617 618 619 /* buffer listener */ 620 621 private val buffer_listener: BufferListener = new BufferAdapter 622 { 623 override def contentInserted(buffer: JEditBuffer, 624 start_line: Int, offset: Int, num_lines: Int, length: Int) 625 { 626 pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length)))) 627 } 628 629 override def preContentRemoved(buffer: JEditBuffer, 630 start_line: Int, offset: Int, num_lines: Int, removed_length: Int) 631 { 632 pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length)))) 633 } 634 } 635 636 637 /* syntax */ 638 639 def syntax_changed() 640 { 641 JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0) 642 for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) 643 Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged"). 644 invoke(text_area) 645 buffer.invalidateCachedFoldLevels 646 } 647 648 def init_token_marker() 649 { 650 Isabelle.buffer_token_marker(buffer) match { 651 case Some(marker) if marker != buffer.getTokenMarker => 652 buffer.setTokenMarker(marker) 653 syntax_changed() 654 case _ => 655 } 656 } 657 658 659 /* init */ 660 661 def init(old_model: Option[File_Model]): Buffer_Model = 662 { 663 GUI_Thread.require {} 664 665 old_model match { 666 case None => 667 pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))) 668 case Some(file_model) => 669 set_node_required(file_model.node_required) 670 pending_edits.set_last_perspective(file_model.last_perspective) 671 pending_edits.edit( 672 file_model.pending_edits ::: 673 Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer))) 674 } 675 676 buffer.addBufferListener(buffer_listener) 677 init_token_marker() 678 679 this 680 } 681 682 683 /* exit */ 684 685 def exit(): File_Model = 686 { 687 GUI_Thread.require {} 688 689 buffer.removeBufferListener(buffer_listener) 690 init_token_marker() 691 692 File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required, 693 pending_edits.get_last_perspective, pending_edits.get_edits) 694 } 695} 696