X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationLexer.ml;h=f5e8ba010b9a625b98297adf41a100adb7d220a4;hb=dee464f8cd331524663167659d1fad01e558d4e1;hp=ce8fcec54b9fba727c1f97c40c6c203029946f72;hpb=d83fa3d6e3604bcc596840219f3998d795630d66;p=helm.git

diff --git a/matitaB/components/content_pres/cicNotationLexer.ml b/matitaB/components/content_pres/cicNotationLexer.ml
index ce8fcec54..f5e8ba010 100644
--- a/matitaB/components/content_pres/cicNotationLexer.ml
+++ b/matitaB/components/content_pres/cicNotationLexer.ml
@@ -73,10 +73,21 @@ let regexp uri =
   ("(" number (',' number)* ")")?  (* reference spec *)
 
 let regexp qstring = '"' [^ '"']* '"'
-let regexp hreftag = "<" [ 'A' 'a' ]
+let regexp xmarkup = '\005'
+let regexp ymarkup = '\006'
+
+let regexp hreftag = xmarkup [ 'A' 'a' ]
 let regexp href = "href=\"" uri "\""
 let regexp hreftitle = "title=" qstring
-let regexp hrefclose = "</" [ 'A' 'a' ] ">"
+let regexp hrefclose = xmarkup "/" [ 'A' 'a' ] ymarkup
+
+let regexp tag_cont = ident_letter | xml_digit | "_" | "-"
+let regexp tagname = ident_letter tag_cont*
+let regexp opentag = xmarkup tagname
+let regexp closetag = xmarkup "/" tagname ymarkup
+let regexp attribute = tagname "=" qstring
+let regexp generictag = 
+  opentag (utf8_blank+ attribute)* ymarkup
 
 let regexp tex_token = '\\' ident
 
@@ -255,6 +266,8 @@ let rec level2_meta_token =
   | utf8_blank+ -> level2_meta_token lexbuf
   | hreftag -> return lexbuf ("ATAG","")
   | hrefclose -> return lexbuf ("ATAGEND","")
+  | generictag
+  | closetag -> level2_meta_token lexbuf
   | ident ->
       handle_keywords lexbuf (fun x -> List.mem x level2_meta_keywords) "IDENT"
   | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
@@ -337,6 +350,8 @@ let level2_ast_token loctable status =
     | placeholder -> return lexbuf ("PLACEHOLDER", "")
     | hreftag -> aux_in_tag None None lexbuf
     | hrefclose -> aux None None lexbuf
+    | generictag 
+    | closetag -> ligatures_token (aux desc href) lexbuf
     | ident -> loctable := 
                  update_table (loc_of_buf lexbuf) desc href !loctable;
                handle_keywords lexbuf (fun x -> StringSet.mem x status) "IDENT"
@@ -399,6 +414,8 @@ let rec level1_pattern_token =
   | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
   | hreftag -> return lexbuf ("ATAG", "")
   | hrefclose -> return lexbuf ("ATAGEND","")
+  | generictag 
+  | closetag -> ligatures_token level1_pattern_token lexbuf
   | ident ->handle_keywords lexbuf (fun x -> List.mem x level1_keywords) "IDENT"
   | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
   | pident->handle_keywords lexbuf (fun x->List.mem x level1_keywords) "PIDENT"