let regexp variable_ident = '_' '_' number
let regexp pident = '_' ident
+let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+
+
+let regexp uri =
+ ("cic:/" | "theory:/") (* schema *)
+(* ident ('/' ident)* |+ path +| *)
+ uri_step ('/' uri_step)* (* path *)
+ ('.' ident)+ (* ext *)
+(* ("#xpointer(" number ('/' number)+ ")")? (* xpointer *) *)
+ ("(" number (',' number)* ")")? (* reference spec *)
+
+let regexp qstring = '"' [^ '"']* '"'
+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 = xmarkup "/" [ 'A' 'a' ] ymarkup
+
+let regexp tag_cont = ident_letter | xml_digit | "_" | "-"
+let regexp gtagname = [ 'B' - 'Z' 'b' - 'z' ] | ident_letter tag_cont+
+let regexp attrname = ident_letter tag_cont*
+let regexp gopentag = xmarkup gtagname
+let regexp closetag = xmarkup "/" gtagname ymarkup
+let regexp attribute = attrname "=" qstring
+let regexp generictag =
+ gopentag (utf8_blank+ attribute)* ymarkup
+
let regexp tex_token = '\\' ident
let regexp delim_begin = "\\["
let regexp ast_csymbol = "@" csymbol
let regexp meta_ident = "$" ident
let regexp meta_anonymous = "$_"
-let regexp qstring = '"' [^ '"']* '"'
let regexp begincomment = "(**" utf8_blank
let regexp beginnote = "(*"
(":=", <:unicode<def>>);
]
-let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+
-
-let regexp uri =
- ("cic:/" | "theory:/") (* schema *)
-(* ident ('/' ident)* |+ path +| *)
- uri_step ('/' uri_step)* (* path *)
- ('.' ident)+ (* ext *)
- ("#xpointer(" number ('/' number)+ ")")? (* xpointer *)
-
let regexp nreference =
"cic:/" (* schema *)
uri_step ('/' uri_step)* (* path *)
let begin_cnum, end_cnum = Ulexing.loc lexbuf in
raise (Error (begin_cnum, end_cnum, msg))
+let loc_of_buf lexbuf =
+ HExtlib.floc_of_loc (Ulexing.loc lexbuf)
+
let return_with_loc token begin_cnum end_cnum =
let flocation = HExtlib.floc_of_loc (begin_cnum,end_cnum) in
token, flocation
let rec level2_meta_token =
lexer
| 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)
Ulexing.rollback lexbuf;
k lexbuf
-let rec level2_ast_token status =
- lexer
- | let_rec -> return lexbuf ("LETREC","")
- | let_corec -> return lexbuf ("LETCOREC","")
- | we_proved -> return lexbuf ("WEPROVED","")
- | we_have -> return lexbuf ("WEHAVE","")
- | utf8_blank+ -> ligatures_token (level2_ast_token status) 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 -> handle_keywords lexbuf (fun x -> StringSet.mem x status) "IDENT"
- | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
- | pident -> handle_keywords lexbuf (fun x -> StringSet.mem x status) "PIDENT"
- | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
- | tex_token -> return lexbuf (expand_macro lexbuf)
- | nreference -> return lexbuf ("NREF", Ulexing.utf8_lexeme lexbuf)
- | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
- | qstring ->
- return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf))
- | csymbol ->
- return lexbuf ("CSYMBOL", remove_left_quote (Ulexing.utf8_lexeme lexbuf))
- | "${" -> read_unparsed_group "UNPARSED_META" lexbuf
- | "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf
- | '(' -> return lexbuf ("LPAREN", "")
- | ')' -> return lexbuf ("RPAREN", "")
- | meta_ident ->
- return lexbuf ("UNPARSED_META",
- remove_left_quote (Ulexing.utf8_lexeme lexbuf))
- | meta_anonymous -> return lexbuf ("UNPARSED_META", "anonymous")
- | beginnote ->
- let _comment = comment_token (Ulexing.utf8_lexeme lexbuf) 0 lexbuf in
-(* let comment =
- Ulexing.utf8_sub_lexeme lexbuf 2 (Ulexing.lexeme_length lexbuf - 4)
- in
- return lexbuf ("NOTE", comment) *)
- ligatures_token (level2_ast_token status) lexbuf
- | begincomment -> return lexbuf ("BEGINCOMMENT","")
- | endcomment -> return lexbuf ("ENDCOMMENT","")
- | eof -> return_eoi lexbuf
- | _ -> return_symbol lexbuf (Ulexing.utf8_lexeme lexbuf)
+module LocalizeOD =
+ struct
+ type t = Stdpp.location
+ let compare = Pervasives.compare
+ end
+
+module LocalizeEnv = Map.Make (LocalizeOD)
+
+let so_pp = function
+ | None -> "()"
+ | Some s -> "*" ^ s
+;;
+
+let update_table loc desc href loctable =
+ if desc <> None || href <> None
+ then
+ (let s,e = HExtlib.loc_of_floc loc in
+
+ prerr_endline (Printf.sprintf "*** [%d,%d] \"%s\",\"%s\""
+ s e (so_pp href) (so_pp desc));
+
+ Printf.printf "*** [%d,%d] \"%s\",\"%s\""
+ s e (so_pp href) (so_pp desc);
+ LocalizeEnv.add loc (href,desc) loctable)
+ else loctable
+;;
-and level1_pattern_token =
+let level2_ast_token loctable status =
+ let rec aux desc href in_tag =
+ lexer
+ | let_rec -> return lexbuf ("LETREC","")
+ | let_corec -> return lexbuf ("LETCOREC","")
+ | we_proved -> return lexbuf ("WEPROVED","")
+ | we_have -> return lexbuf ("WEHAVE","")
+ | utf8_blank+ -> ligatures_token (aux desc href in_tag) 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", "")
+ | hreftag -> aux_attr None None lexbuf
+ | hrefclose -> return lexbuf ("LEXING_ERROR", Ulexing.utf8_lexeme lexbuf)
+ (* ignore other tags *)
+ | generictag
+ | closetag -> ligatures_token (aux desc href in_tag) lexbuf
+ | ident -> if in_tag then
+ aux_close_tag desc href ("IDENT", Ulexing.utf8_lexeme lexbuf) lexbuf
+ else handle_keywords lexbuf (fun x -> StringSet.mem x status) "IDENT"
+ | variable_ident ->
+ return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
+ | pident -> if in_tag then
+ aux_close_tag desc href ("PIDENT", Ulexing.utf8_lexeme lexbuf) lexbuf
+ else handle_keywords lexbuf (fun x -> StringSet.mem x status) "PIDENT"
+ | number -> let token = "NUMBER", Ulexing.utf8_lexeme lexbuf
+ in
+ if in_tag then
+ aux_close_tag desc href token lexbuf
+ else return lexbuf token
+ | tex_token -> let token = expand_macro lexbuf
+ in
+ if in_tag then
+ aux_close_tag desc href token lexbuf
+ else return lexbuf token
+ | nreference -> return lexbuf ("NREF", Ulexing.utf8_lexeme lexbuf)
+ | uri -> return lexbuf ("URI", Ulexing.utf8_lexeme lexbuf)
+ | qstring ->
+ return lexbuf ("QSTRING", remove_quotes (Ulexing.utf8_lexeme lexbuf))
+ | csymbol ->
+ return lexbuf ("CSYMBOL", remove_left_quote (Ulexing.utf8_lexeme lexbuf))
+ | "${" -> read_unparsed_group "UNPARSED_META" lexbuf
+ | "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf
+ | '(' -> return lexbuf ("LPAREN", "")
+ | ')' -> return lexbuf ("RPAREN", "")
+ | meta_ident ->
+ return lexbuf ("UNPARSED_META",
+ remove_left_quote (Ulexing.utf8_lexeme lexbuf))
+ | meta_anonymous -> return lexbuf ("UNPARSED_META", "anonymous")
+ | beginnote ->
+ let _comment = comment_token (Ulexing.utf8_lexeme lexbuf) 0 lexbuf in
+ (* let comment =
+ Ulexing.utf8_sub_lexeme lexbuf 2 (Ulexing.lexeme_length lexbuf - 4)
+ in
+ return lexbuf ("NOTE", comment) *)
+ ligatures_token (aux desc href in_tag) lexbuf
+ | begincomment -> return lexbuf ("BEGINCOMMENT","")
+ | endcomment -> return lexbuf ("ENDCOMMENT","")
+ | eof -> return_eoi lexbuf
+ | _ -> let token = "SYMBOL", (Ulexing.utf8_lexeme lexbuf)
+ in
+ if in_tag then
+ aux_close_tag desc href token lexbuf
+ else return lexbuf token
+
+ and aux_attr desc href = lexer
+ | utf8_blank+ -> ligatures_token (aux_attr desc href) lexbuf
+ | href ->
+ aux_attr desc
+ (Some (Ulexing.utf8_sub_lexeme lexbuf 6 (Ulexing.lexeme_length lexbuf - 7)))
+ lexbuf
+ | hreftitle ->
+ aux_attr
+ (Some (Ulexing.utf8_sub_lexeme lexbuf 7 (Ulexing.lexeme_length lexbuf - 8)))
+ href lexbuf
+ | ymarkup -> aux desc href true lexbuf
+ | _ -> return lexbuf ("LEXING_ERROR", Ulexing.utf8_lexeme lexbuf)
+
+(* and aux_in_tag desc href = lexer
+ | ident -> loctable :=
+ update_table (loc_of_buf lexbuf) desc href !loctable;
+ handle_keywords lexbuf (fun x -> StringSet.mem x status) "IDENT"
+ | variable_ident ->
+ return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
+ | pident -> loctable :=
+ update_table (loc_of_buf lexbuf) desc href !loctable;
+ handle_keywords lexbuf (fun x -> StringSet.mem x status) "PIDENT"
+ | number -> loctable :=
+ update_table (loc_of_buf lexbuf) desc href !loctable;
+ return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
+ | tex_token -> loctable :=
+ update_table (loc_of_buf lexbuf) desc href !loctable;
+ return lexbuf (expand_macro lexbuf)
+ | _ -> loctable :=
+ update_table (loc_of_buf lexbuf) desc href !loctable;
+ return_symbol lexbuf (Ulexing.utf8_lexeme lexbuf)
+ *)
+ and aux_close_tag desc href token = lexer
+ | hrefclose -> loctable := update_table (loc_of_buf lexbuf) desc href !loctable;
+ return lexbuf token
+ | _ -> return lexbuf ("LEXING_ERROR", Ulexing.utf8_lexeme lexbuf)
+ in aux None None false
+
+let rec level1_pattern_token =
lexer
| utf8_blank+ -> ligatures_token level1_pattern_token lexbuf
| number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
- | ident ->handle_keywords lexbuf (fun x -> List.mem x level1_keywords) "IDENT"
+ | 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"
| color -> return lexbuf ("COLOR", Ulexing.utf8_lexeme lexbuf)
| _ -> return_symbol lexbuf (Ulexing.utf8_lexeme lexbuf)
let level1_pattern_token = ligatures_token level1_pattern_token
-let level2_ast_token status = ligatures_token (level2_ast_token status)
+let level2_ast_token loctable status =
+ ligatures_token (level2_ast_token loctable status)
(* API implementation *)
type lexers = {
level2_meta_lexer : (string * string) Token.glexer
}
-let mk_lexers keywords =
+let mk_lexers loctable keywords =
let initial_keywords =
[ "CProp"; "Prop"; "Type"; "Set"; "let"; "match";
"with"; "in"; "and"; "to"; "as"; "on"; "return"; "done" ]
in
{
level1_pattern_lexer = mk_lexer level1_pattern_token;
- level2_ast_lexer = mk_lexer (level2_ast_token status);
+ level2_ast_lexer = mk_lexer (level2_ast_token loctable status);
level2_meta_lexer = mk_lexer level2_meta_token
}
;;
projects / helm.git / blobdiff