]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/cicNotationLexer.ml
- cicInspect: relevant nodes count updated: letin nodes are not relevant
[helm.git] / helm / software / components / content_pres / cicNotationLexer.ml
index 71ea77731411c3fad02d186c5138ecf937439821..17a5bd5bbdebc7f3a5d61876ece74478d9a34474 100644 (file)
@@ -210,7 +210,9 @@ let expand_macro lexbuf =
   in
   try
     ("SYMBOL", Utf8Macro.expand macro)
-  with Utf8Macro.Macro_not_found _ -> "SYMBOL", Ulexing.utf8_lexeme lexbuf
+  with Utf8Macro.Macro_not_found _ -> 
+(* FG: unexpanded TeX macros are terminated by a space for rendering *)     
+     "SYMBOL", (Ulexing.utf8_lexeme lexbuf ^ " ")
 
 let remove_quotes s = String.sub s 1 (String.length s - 2)
 let remove_left_quote s = String.sub s 1 (String.length s - 1)