# HG changeset patch
# User blanchet
# Date 1343393797 -7200
# Node ID be4bf5f6b2ef9f1a196c20fdda97094aabe1e137
# Parent  122e67e77493718024bdf841cd5a71f401b5abb1
nicer Nitpick subscript output in jEdit

diff -r 122e67e77493 -r be4bf5f6b2ef src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Jul 27 08:52:40 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Jul 27 14:56:37 2012 +0200
@@ -237,17 +237,9 @@
 val parse_time_option = Sledgehammer_Util.parse_time_option
 val string_from_time = ATP_Util.string_from_time
 
-val i_subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
-fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
+val i_subscript = implode o map (prefix "\<^isub>") o Symbol.explode
 fun nat_subscript n =
-  let val s = signed_string_of_int n in
-    if print_mode_active Symbol.xsymbolsN then
-      (* cheap trick to ensure proper alphanumeric ordering for one- and
-         two-digit numbers *)
-      (if n <= 9 then be_subscript else i_subscript) s
-    else
-      s
-  end
+  n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? i_subscript
 
 fun flip_polarity Pos = Neg
   | flip_polarity Neg = Pos