src/Tools/jEdit/src/document_view.scala
changeset 47027 fc3bb6c02a3c
parent 47013 95bd95addb24
child 47392 6a08fd7a6071
equal deleted inserted replaced
47026:36dacca8a95c 47027:fc3bb6c02a3c
   142       model.update_perspective()
   142       model.update_perspective()
   143     }
   143     }
   144   }
   144   }
   145 
   145 
   146 
   146 
   147   /* snapshot */
       
   148 
       
   149   // owned by Swing thread
       
   150   @volatile private var was_outdated = false
       
   151   @volatile private var was_updated = false
       
   152 
       
   153   def update_snapshot(): Document.Snapshot =
       
   154   {
       
   155     Swing_Thread.require()
       
   156     val snapshot = model.snapshot()
       
   157     was_updated &&= !snapshot.is_outdated
       
   158     was_outdated ||= snapshot.is_outdated
       
   159     snapshot
       
   160   }
       
   161 
       
   162   def flush_snapshot(): (Boolean, Document.Snapshot) =
       
   163   {
       
   164     Swing_Thread.require()
       
   165     val snapshot = update_snapshot()
       
   166     val updated = was_updated
       
   167     if (updated) { was_outdated = false; was_updated = false }
       
   168     (updated, snapshot)
       
   169   }
       
   170 
       
   171 
       
   172   /* HTML popups */
   147   /* HTML popups */
   173 
   148 
   174   private var html_popup: Option[Popup] = None
   149   private var html_popup: Option[Popup] = None
   175 
   150 
   176   private def exit_popup() { html_popup.map(_.hide) }
   151   private def exit_popup() { html_popup.map(_.hide) }
   240       val y = e.getY()
   215       val y = e.getY()
   241 
   216 
   242       if (!model.buffer.isLoaded) exit_control()
   217       if (!model.buffer.isLoaded) exit_control()
   243       else
   218       else
   244         Isabelle.buffer_lock(model.buffer) {
   219         Isabelle.buffer_lock(model.buffer) {
   245           val snapshot = update_snapshot()
   220           val snapshot = model.snapshot()
   246 
   221 
   247           if (control) init_popup(snapshot, x, y)
   222           if (control) init_popup(snapshot, x, y)
   248 
   223 
   249           for (Text.Info(range, _) <- _highlight_range) invalidate_range(range)
   224           for (Text.Info(range, _) <- _highlight_range) invalidate_range(range)
   250           _highlight_range =
   225           _highlight_range =
   266   private val tooltip_painter = new TextAreaExtension
   241   private val tooltip_painter = new TextAreaExtension
   267   {
   242   {
   268     override def getToolTipText(x: Int, y: Int): String =
   243     override def getToolTipText(x: Int, y: Int): String =
   269     {
   244     {
   270       robust_body(null: String) {
   245       robust_body(null: String) {
   271         val snapshot = update_snapshot()
   246         val snapshot = model.snapshot()
   272         val offset = text_area.xyToOffset(x, y)
   247         val offset = text_area.xyToOffset(x, y)
   273         val range = Text.Range(offset, offset + 1)
   248         val range = Text.Range(offset, offset + 1)
   274         val tip =
   249         val tip =
   275           if (control) Isabelle_Rendering.tooltip(snapshot, range)
   250           if (control) Isabelle_Rendering.tooltip(snapshot, range)
   276           else Isabelle_Rendering.tooltip_message(snapshot, range)
   251           else Isabelle_Rendering.tooltip_message(snapshot, range)
   293         val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
   268         val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
   294         val FOLD_MARKER_SIZE = 12
   269         val FOLD_MARKER_SIZE = 12
   295 
   270 
   296         if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
   271         if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
   297           Isabelle.buffer_lock(model.buffer) {
   272           Isabelle.buffer_lock(model.buffer) {
   298             val snapshot = update_snapshot()
   273             val snapshot = model.snapshot()
   299             for (i <- 0 until physical_lines.length) {
   274             for (i <- 0 until physical_lines.length) {
   300               if (physical_lines(i) != -1) {
   275               if (physical_lines(i) != -1) {
   301                 val line_range = proper_line_range(start(i), end(i))
   276                 val line_range = proper_line_range(start(i), end(i))
   302 
   277 
   303                 // gutter icons
   278                 // gutter icons
   338   /* caret handling */
   313   /* caret handling */
   339 
   314 
   340   def selected_command(): Option[Command] =
   315   def selected_command(): Option[Command] =
   341   {
   316   {
   342     Swing_Thread.require()
   317     Swing_Thread.require()
   343     update_snapshot().node.command_at(text_area.getCaretPosition).map(_._1)
   318     model.snapshot().node.command_at(text_area.getCaretPosition).map(_._1)
   344   }
   319   }
   345 
   320 
   346   private val delay_caret_update =
   321   private val delay_caret_update =
   347     Swing_Thread.delay_last(session.input_delay) {
   322     Swing_Thread.delay_last(session.input_delay) {
   348       session.caret_focus.event(Session.Caret_Focus)
   323       session.caret_focus.event(Session.Caret_Focus)
   370         case changed: Session.Commands_Changed =>
   345         case changed: Session.Commands_Changed =>
   371           val buffer = model.buffer
   346           val buffer = model.buffer
   372           Swing_Thread.later {
   347           Swing_Thread.later {
   373             Isabelle.buffer_lock(buffer) {
   348             Isabelle.buffer_lock(buffer) {
   374               if (model.buffer == text_area.getBuffer) {
   349               if (model.buffer == text_area.getBuffer) {
   375                 val (updated, snapshot) = flush_snapshot()
   350                 val snapshot = model.snapshot()
   376 
   351 
   377                 if (updated ||
   352                 if (changed.assignment ||
   378                     (changed.nodes.contains(model.name) &&
   353                     (changed.nodes.contains(model.name) &&
   379                      changed.commands.exists(snapshot.node.commands.contains)))
   354                      changed.commands.exists(snapshot.node.commands.contains)))
   380                   overview.delay_repaint(true)
   355                   overview.delay_repaint(true)
   381 
   356 
   382                 visible_range() match {
   357                 visible_range() match {
   383                   case Some(visible) =>
   358                   case Some(visible) =>
   384                     if (updated) invalidate_range(visible)
   359                     if (changed.assignment) invalidate_range(visible)
   385                     else {
   360                     else {
   386                       val visible_cmds =
   361                       val visible_cmds =
   387                         snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
   362                         snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
   388                       if (visible_cmds.exists(changed.commands)) {
   363                       if (visible_cmds.exists(changed.commands)) {
   389                         for {
   364                         for {