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