Re: [isabelle] Superscript argument to a function



Dear Pedro,

I tried updating the patch to the current development version (attached as ‹sub_sup_devel.patch›). After straightforward rebasing it worked for me seemingly correctly. I did not fully understand the issue with nested scripts, though. If you mean *long* (delimited, multi-symbol) sub/superscripts, their nesting was actually not supported in the original patch in a sense that nested script delimiters were hidden, but ignored, and so the inner font style was unchanged (as to visually merge with the outer script). Only one-symbol nested scripted were supported. I tried modifying the patch to support nested delimited scripts (attached ‹sub_sup_stack.patch›) and it also seems to work (on small artificial tests), but I have not tested it on any realistic examples yet

Regards,
Mikhail

Pedro Sánchez Terraf писал 2021-09-07 17:06:
Dear Mikhail,

I've been successfully using your patch on Isabelle2020. Though I
tried hard, I couldn't make it work for the current development
version (I only managed to make it work with non-nested scripts).
Would you mind giving me some hints on how to adapt it?

I'm about to present a formalization to other mathematicians and a
smooth notation is key.

Thank you very much in advance,
--
Pedro Sánchez Terraf
CIEM-FAMAF — Universidad Nacional de Córdoba
cs.famaf.unc.edu.ar/~pedro [3]

On 18/8/20 19:51, Mikhail Mandrykin wrote:

Hello,

Concerning applying the patch, I’m not familiar with hg but in
git I’d
try checking out the commit mentioned in the path, apply it there
and
hope for merge to do it’s magic.
Just in case I adapted the patch for Isabelle 2020 (last relevant
commit 97ccf48c2f0c) and it works for me on some non-trivial
theories with nested subscripts and superscripts (I also don't have
any previous experience with Isabelle/Scala though)

Sample original theory source fragment:
⬚‹
also from Sucinner have
"... = - G κ⇘i+1⇙ κ⇘i+2⇙
+ int (∑x|x<m⇘κ⇘i+1⇙⇙∧x⇧♮∈vars
K⇘κ⇘i+1⇙⇙.
MAX⇩0 t∈terms
K⇘κ⇘i+1⇙⇙|t~P⇘κ⇘i+2⇙⇙!0. #⇘x⇧♮⇙ t * size
(σ⇘i+1⇙ x⇧♮))
- int (∑x≤(m⇘κ⇘i+1⇙⇙ - 1)⇧♯. #⇩x
(P⇘κ⇘i+1⇙⇙!0) * size (σ⇘i+1⇙ x))"
(is "_ + int (∑x∈?S. ?g x) - _ = _ + int (∑x∈?T. ?h x)-
_") by
›

Regards,
Mikhail

Benedikt Nordhoff писал 2020-08-13 14:33:

Dear Pedro,

I’m certainly not the most qualified to answer this. I haven’t
build
Isabelle from source for quite a while. I think back then I used
the
README_REPOSITORY file as a guide.

Best Benedikt

Am 12.08.2020 um 17:36 schrieb Pedro Sánchez Terraf
<sterraf at famaf.unc.edu.ar>:

Dear Benedikt,

Sorry to bother you with an dumb question, but I do not know how to
build jEdit. Could you point me to some docs where I can find this?
(Note: I'm not a computer scientist but I can manage some stuff).
It seems that there have been many some movements and the patch
should be applied somewhere in

Tools/jEdit/src/syntax_style.scala,
but I could be wrong.

Best wishes,
PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html> [1]

El 10/8/20 a las 04:27, Benedikt Nordhoff escribió:
Dear Pedro,

I implemented basic support for this for Isabelle 2014 but it never
made it into any release. It worked fine till the 2017 release, I
haven’t tried the patch on later versions. If you’re interested
and want to try whether the patch still works you can find it here:

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-August/msg00214.html

<https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-August/msg00214.html>
[2]

Best
Benedikt

Am 28.07.2020 um 15:45 schrieb Pedro Sánchez Terraf
<sterraf at famaf.unc.edu.ar> <mailto:sterraf at famaf.unc.edu.ar>:

Good day,

I have a question concerning the use of superscripts as arguments to
functions. I have a function ccc_rel that has 3 arguments, and I
would like that the syntax for the first one is a superscript. (I'm
working in ZF, don't know if that is relevant.)

If I enter

notation ccc_rel (‹ccc⇧_'(_,_')›)

everything works fine *until* the first argument has more than one
character. If I use \<bsup>...\<esup> instead:

notation ccc_rel (‹ccc⇗_⇖'(_,_')›)

it accepts a multi-character first argument but it the PIDE does not
prettyprints the superscript.

Can I have the cake and eat it?

PST.-
cs.famaf.unc.edu.ar/~pedro/home_en
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html> [1]
<https://cs.famaf.unc.edu.ar/~pedro/home_en.html> [1]


Links:
------
[1] https://cs.famaf.unc.edu.ar/~pedro/home_en.html
[2] https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-August/msg00214.html
[3] https://cs.famaf.unc.edu.ar/~pedro
diff -r be49c660ebbf src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala	Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala	Wed Sep 08 11:47:11 2021 +0300
@@ -1,5 +1,6 @@
 /*  Title:      Tools/jEdit/src/syntax_style.scala
     Author:     Makarius
+    Author:     Benedikt Nordhoff
 
 Support for extended syntax styles: subscript, superscript, bold, user fonts.
 */
@@ -127,40 +128,140 @@
 
   def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] =
   {
+    // Counters for nesting level of bsub/esub resp. bsup/esup
+    var subcnt = 0
+    var supcnt = 0
+
+    // Active control region
+    val NONE = 0
+    val SUB = 1
+    val SUP = 2
+    var active_control = NONE
+
+    // Control style to apply
+    var style: Option[Byte => Byte] = None
+
+    // Offset to hide before next char 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() : Unit = {
+      subcnt = 0
+      supcnt = 0
+      active_control = NONE
+      style = 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 == SUB && sym == ESUB_SYM || supcnt == 0 && active_control == SUP && sym == ESUP_SYM
+
+    // Calculates next control state
+    def update_control(sym: String) : Unit = {
+      hide_if_active = 0
+      if (active_control == NONE) {
+        sym match {
+          case SUB_SYM => style = Some(subscript)
+          case SUP_SYM => style = Some(superscript)
+          case BOLD_SYM => style = Some(bold)
+          case BSUB_SYM => style = Some(subscript); active_control = SUB
+          case BSUP_SYM => style = Some(superscript); active_control = SUP
+          case _ => style = None
+        }
+        if (is_control_to_hide_later(sym)) hide_if_active = sym.length
+      } else if (active_control == SUB) {
+        sym match {
+          case ESUB_SYM if (subcnt == 0) => style = None; active_control = NONE
+          case SUB_SYM => style = Some(subscript)
+          case SUP_SYM => style = Some(superscript)
+          case _ => style = Some(subscript)
+        }
+        if (is_control_to_hide_later(sym)) hide_if_active = sym.length
+      } else if (active_control == SUP) {
+        sym match {
+          case ESUP_SYM if (supcnt == 0) => style = None; active_control = NONE
+          case SUB_SYM => style = Some(subscript)
+          case SUP_SYM => style = Some(superscript)
+          case _ => style = Some(superscript)
+        }
+        if (is_control_to_hide_later(sym)) hide_if_active = sym.length
+      }
+    }
+
+    // Updates conuters for control nesting
+    def update_counter(sym: String) : Unit = {
+      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): Unit =
     {
       for (i <- start until stop) result += (i -> style)
     }
 
-    var offset = 0
-    var control_sym = ""
-    for (sym <- Symbol.iterator(text)) {
-      val end_offset = offset + sym.length
-
-      if (control_style(sym).isDefined) control_sym = sym
-      else if (control_sym != "") {
-        if (Symbol.is_controllable(sym) && !Symbol.fonts.isDefinedAt(sym)) {
-          mark(offset - control_sym.length, offset, _ => hidden)
-          mark(offset, end_offset, control_style(control_sym).get)
+    def apply_control(sym: String, offset: Text.Offset) : Unit = {
+      if (is_active_end(sym)) {
+        // Hide control symbol closing the active control area
+        mark(offset, offset + sym.length, _ => hidden)
+      } else if (is_control_end(sym)) {
+        // Hide control closing symbol inside the active control area
+        mark(offset, offset + sym.length, _ => hidden)
+      } else if (style.isDefined &&
+                 (Symbol.is_controllable(sym) &&
+                  sym != "\"" &&
+                  !Symbol.fonts.isDefinedAt(sym) ||
+                  sym == BOLD_SYM)) {
+        // Control is active hide possible leading control symbol
+        if (hide_if_active > 0) {
+          mark(offset - hide_if_active, offset, _ => hidden)
         }
-        control_sym = ""
-      }
-
-      if (Symbol.is_control_encoded(sym)) {
+        // Apply control style
+        mark(offset, offset + sym.length, style.get)
+      } else if (Symbol.is_control_encoded(sym)) {
+        val end_offset = offset + sym.length
         val a = offset + Symbol.control_prefix.length
         val b = end_offset - Symbol.control_suffix.length
         mark(offset, a, _ => hidden)
         mark(a, b, _ => control)
         mark(b, end_offset, _ => hidden)
+      } else {
+        Symbol.lookup_font(sym) match {
+          case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
+          case _ =>
+        }
       }
+    }
 
-      Symbol.lookup_font(sym) match {
-        case Some(idx) => mark(offset, end_offset, user_font(idx, _))
-        case _ =>
-      }
+    def process_symbol(sym: String, offset: Text.Offset) : Unit = {
+      if (sym == "\"") reset_control()
+      update_counter(sym)
+      apply_control(sym, offset)
+      update_control(sym)
+    }
 
-      offset = end_offset
+    var offset = 0
+    reset_control()
+    for (sym <- Symbol.iterator(text)) {
+      process_symbol(sym, offset)
+      offset += sym.length
     }
 
     result
diff -r be49c660ebbf src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala	Tue Sep 07 22:35:44 2021 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala	Wed Sep 08 13:10:55 2021 +0300
@@ -1,5 +1,6 @@
 /*  Title:      Tools/jEdit/src/syntax_style.scala
     Author:     Makarius
+    Author:     Benedikt Nordhoff
 
 Support for extended syntax styles: subscript, superscript, bold, user fonts.
 */
@@ -9,6 +10,8 @@
 
 import isabelle._
 
+import scala.collection.mutable.Stack
+
 import java.util.{Map => JMap}
 import java.awt.{Font, Color}
 import java.awt.font.TextAttribute
@@ -127,40 +130,124 @@
 
   def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] =
   {
+
+    // Active control region
+    val SUB = 0
+    val SUP = 1
+    var active_control = Stack[Int]()
+
+    // Control style to apply
+    var style: Option[Byte => Byte] = None
+
+    // Offset to hide before next char 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() : Unit = {
+      active_control.clear()
+      style = 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) =
+      active_control.headOption == Some(SUB) && sym == ESUB_SYM ||
+      active_control.headOption == Some(SUP) && sym == ESUP_SYM
+
+    def restore_style() : Option[Byte => Byte] = {
+      if (active_control.isEmpty) None
+      else if (active_control.head == SUB) Some(subscript)
+      else if (active_control.head == SUP) Some(superscript)
+      else error ("Wrong active control state: " + active_control)
+    }
+
+    // Calculates next control state
+    def update_control(sym: String) : Unit = {
+      hide_if_active = 0
+      if (active_control.isEmpty) {
+        sym match {
+          case SUB_SYM => style = Some(subscript)
+          case SUP_SYM => style = Some(superscript)
+          case BOLD_SYM => style = Some(bold)
+          case BSUB_SYM => style = Some(subscript); active_control.push(SUB)
+          case BSUP_SYM => style = Some(superscript); active_control.push(SUP)
+          case _ => style = None
+        }
+        if (is_control_to_hide_later(sym)) hide_if_active = sym.length
+      } else {
+        sym match {
+          case SUB_SYM => style = Some(subscript)
+          case SUP_SYM => style = Some(superscript)
+          case BSUB_SYM => style = Some(subscript); active_control.push(SUB)
+          case BSUP_SYM => style = Some(superscript); active_control.push(SUP)
+          case ESUB_SYM | ESUP_SYM => active_control.pop(); style = restore_style()
+          case _ => style = restore_style()
+        }
+        if (is_control_to_hide_later(sym)) hide_if_active = sym.length
+      }
+    }
+
     var result = Map[Text.Offset, Byte => Byte]()
     def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte): Unit =
     {
       for (i <- start until stop) result += (i -> style)
     }
 
-    var offset = 0
-    var control_sym = ""
-    for (sym <- Symbol.iterator(text)) {
-      val end_offset = offset + sym.length
-
-      if (control_style(sym).isDefined) control_sym = sym
-      else if (control_sym != "") {
-        if (Symbol.is_controllable(sym) && !Symbol.fonts.isDefinedAt(sym)) {
-          mark(offset - control_sym.length, offset, _ => hidden)
-          mark(offset, end_offset, control_style(control_sym).get)
+    def apply_control(sym: String, offset: Text.Offset) : Unit = {
+      if (is_active_end(sym)) {
+        // Hide control symbol closing the active control area
+        mark(offset, offset + sym.length, _ => hidden)
+      } else if (is_control_end(sym)) {
+        // Hide control closing symbol inside the active control area
+        mark(offset, offset + sym.length, _ => hidden)
+      } else if (style.isDefined &&
+                 (Symbol.is_controllable(sym) &&
+                  sym != "\"" &&
+                  !Symbol.fonts.isDefinedAt(sym) ||
+                  sym == BOLD_SYM)) {
+        // Control is active hide possible leading control symbol
+        if (hide_if_active > 0) {
+          mark(offset - hide_if_active, offset, _ => hidden)
         }
-        control_sym = ""
-      }
-
-      if (Symbol.is_control_encoded(sym)) {
+        // Apply control style
+        mark(offset, offset + sym.length, style.get)
+      } else if (Symbol.is_control_encoded(sym)) {
+        val end_offset = offset + sym.length
         val a = offset + Symbol.control_prefix.length
         val b = end_offset - Symbol.control_suffix.length
         mark(offset, a, _ => hidden)
         mark(a, b, _ => control)
         mark(b, end_offset, _ => hidden)
+      } else {
+        Symbol.lookup_font(sym) match {
+          case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
+          case _ =>
+        }
       }
+    }
 
-      Symbol.lookup_font(sym) match {
-        case Some(idx) => mark(offset, end_offset, user_font(idx, _))
-        case _ =>
-      }
+    def process_symbol(sym: String, offset: Text.Offset) : Unit = {
+      if (sym == "\"") reset_control()
+      apply_control(sym, offset)
+      update_control(sym)
+    }
 
-      offset = end_offset
+    var offset = 0
+    reset_control()
+    for (sym <- Symbol.iterator(text)) {
+      process_symbol(sym, offset)
+      offset += sym.length
     }
 
     result


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