[isabelle] Experimental Isabelle/jEdit support for bsup/esup + bsub/esub



Dear Isabelle developers,

earlier today I was frustrated again to have no /approximate/ rendering of bsup/esup in Isabelle/jEdit. I therefore spent the evening digging into the Isabelle source code for the first time and came up with the attached _experimental_ /solution/. It applies the outermost control and and prints control symbols for inner ones.

It works well for my use cases and I didn't observe any problems so far.

But probably this will break everything somewhere else as I'm not aware in which contexts the modified code is used. So Makarius could have a look if he likes. I didn't figure out how update/edit_control_style are used and whether that may cause any problems.

I'll be happy if you give it a test run and have any comments.

Best
    Benedikt
# HG changeset patch
# User Benedikt Nordhoff
# Date 1408735070 -7200
#      Fri Aug 22 21:17:50 2014 +0200
# Node ID 849fb4e77aaf51749b0639796467f78984342ee3
# Parent  177eeda93a8cc4c89d59f252e8c10a64b634fbd0
Experimental support for bsup/esup resp. bsub/esub.

diff -r 177eeda93a8c -r 849fb4e77aaf src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Fri Aug 22 17:35:48 2014 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Fri Aug 22 21:17:50 2014 +0200
@@ -1,6 +1,6 @@
 /*  Title:      Tools/jEdit/src/token_markup.scala
     Author:     Makarius
-
+    Author:     Benedikt Nordhoff
 Outer syntax token markup.
 */
 
@@ -69,7 +69,7 @@
 
 
   /* extended syntax styles */
-
+  
   private val plain_range: Int = JEditToken.ID_COUNT
   private val full_range = 6 * plain_range + 1
   private def check_range(i: Int) { require(0 <= i && i < plain_range) }
@@ -140,33 +140,120 @@
 
   def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] =
   {
-    // FIXME Symbol.bsub_decoded etc.
-    def control_style(sym: String): Option[Byte => Byte] =
-      if (sym == Symbol.sub_decoded) Some(subscript(_))
-      else if (sym == Symbol.sup_decoded) Some(superscript(_))
-      else if (sym == Symbol.bold_decoded) Some(bold(_))
-      else None
+
+    // Counters for nesting level of bsub/esub resp. bsup/esup
+    var subcnt = 0
+    var supcnt = 0
+
+    // Active control region: 0 = none, 1 = subscript, 2 = superscript
+    var active_control = 0
+
+    // Control style to apply
+    var control : Option[Byte => Byte] = None
+    
+    // Offset to hide before next chare if control becomes active
+    var hide_if_active = 0
+
+    // Copy to stable identifiers to allow case distinctions
+    val SUB_SYM = Symbol.sub_decoded
+    val SUP_SYM = Symbol.sup_decoded
+    val BOLD_SYM = Symbol.bold_decoded
+    val BSUB_SYM = Symbol.bsub_decoded
+    val BSUP_SYM = Symbol.bsup_decoded
+    val ESUB_SYM = Symbol.esub_decoded
+    val ESUP_SYM = Symbol.esup_decoded
+
+    val is_control_to_hide_later = Set (SUB_SYM, SUP_SYM, BOLD_SYM, BSUB_SYM, BSUP_SYM)
+    val is_control_end = Set (ESUB_SYM, ESUP_SYM)
+
+    def reset_control() {
+      subcnt = 0
+      supcnt = 0
+      active_control = 0
+      control = None
+      hide_if_active = 0
+    }
+
+    // Check whether a control symbols terminates the active control, used to hide symbol if so
+    def is_active_end(sym: String) = 
+      subcnt == 0 && active_control == 1 && sym == ESUB_SYM || supcnt == 0 && active_control == 2 && sym == ESUP_SYM
+
+    // Calculates next control state
+    def update_control(sym: String) {
+      hide_if_active = 0
+      if(active_control == 0) {
+        sym match {
+          case SUB_SYM => control = Some(subscript(_)) 
+          case SUP_SYM => control = Some(superscript(_))
+          case BOLD_SYM => control = Some(bold(_))
+          case BSUB_SYM => control = Some(subscript(_)); active_control = 1
+          case BSUP_SYM => control = Some(superscript(_)); active_control = 2
+          case _ => control = None
+        }
+	if (is_control_to_hide_later(sym)) hide_if_active = sym.length
+      } 
+      else if (active_control == 1) {
+        sym match {          
+          case ESUB_SYM if (subcnt == 0) => control = None; active_control = 0
+          case _ => control = Some(subscript(_))
+        }
+      }
+      else if (active_control == 2) {
+        sym match {          
+          case ESUP_SYM if (supcnt == 0) => control = None; active_control = 0
+          case _ => control = Some(superscript(_))
+        }
+      } 
+    }
+
+    // Updates conuters for control nesting
+    def update_counter(sym: String) {
+      sym match {
+        case BSUB_SYM => subcnt += 1
+        case BSUP_SYM => supcnt += 1
+        case ESUB_SYM => if(subcnt > 0) subcnt -= 1
+        case ESUP_SYM => if(supcnt > 0) supcnt -= 1
+        case _ => 
+      }
+    }
 
     var result = Map[Text.Offset, Byte => Byte]()
     def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
     {
       for (i <- start until stop) result += (i -> style)
     }
+
+    def apply_control(sym: String, offset: Text.Offset) {
+      if(is_active_end(sym)) {
+        // Hide control symbol closing the active control area
+        mark(offset, offset + sym.length, _ => hidden)
+      } 
+      else if(control.isDefined && Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) {
+        // Control is active hide possible leading control symbol
+        if(hide_if_active > 0) {
+          mark(offset - hide_if_active, offset, _ => hidden)
+        }
+        // Apply control style
+        mark(offset, offset + sym.length, control.get)
+      } else {              
+        Symbol.lookup_font(sym) match {
+          case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
+          case _ =>
+        }
+      }
+    }
+
+    def process_symbol(sym: String, offset:Text.Offset) {
+      if(sym == "\"") reset_control()
+      update_counter(sym)
+      apply_control(sym,offset)      
+      update_control(sym)
+    }
+    
     var offset = 0
-    var control = ""
+    reset_control()
     for (sym <- Symbol.iterator(text)) {
-      if (control_style(sym).isDefined) control = sym
-      else if (control != "") {
-        if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) {
-          mark(offset - control.length, offset, _ => hidden)
-          mark(offset, offset + sym.length, control_style(control).get)
-        }
-        control = ""
-      }
-      Symbol.lookup_font(sym) match {
-        case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
-        case _ =>
-      }
+      process_symbol(sym, offset)
       offset += sym.length
     }
     result


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.