proper treatment of empty name -- avoid excessive vertical space;
authorwenzelm
Tue, 03 May 2011 20:59:24 +0200
changeset 42661 824d3f1d8de6
parent 42660 e40648514b34
child 42662 2080fe35abea
proper treatment of empty name -- avoid excessive vertical space;
src/Pure/Thy/rail.ML
--- a/src/Pure/Thy/rail.ML	Tue May 03 20:58:42 2011 +0200
+++ b/src/Pure/Thy/rail.ML	Tue May 03 20:59:24 2011 +0200
@@ -242,7 +242,8 @@
         val (rail', y') = vertical_range rail 0;
         val out_name =
           (case name of
-            Antiquote.Text s => output_text false s
+            Antiquote.Text "" => ""
+          | Antiquote.Text s => output_text false s
           | Antiquote.Antiq a => output_antiq a);
       in
         "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^