X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationLexer.ml;h=67340d37a255662b1270a26ce757c18d82768de7;hb=8d55798c22b29c00febc623234db5f57483c0401;hp=8848a3ce5045b4648e1d3f8b49fe5db27444e931;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml index 8848a3ce5..67340d37a 100644 --- a/helm/software/components/content_pres/cicNotationLexer.ml +++ b/helm/software/components/content_pres/cicNotationLexer.ml @@ -279,7 +279,9 @@ let rec ligatures_token k = and level2_ast_token = lexer | xml_blank+ -> ligatures_token level2_ast_token lexbuf - | meta -> return lexbuf ("META", Ulexing.utf8_lexeme lexbuf) + | meta -> + let s = Ulexing.utf8_lexeme lexbuf in + return lexbuf ("META", String.sub s 1 (String.length s - 1)) | implicit -> return lexbuf ("IMPLICIT", "") | placeholder -> return lexbuf ("PLACEHOLDER", "") | ident ->