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)
-let print = Printf.fprintf
+let print s t = s := (!s ^ t) (* Printf.fprintf *)
+
+let xmarkup = "\005"
+let ymarkup = "\006"
let handle_full_id ch id uri =
- print ch "<A href=\"%s\">%s</A>" uri id
+ let id' = Printf.sprintf "\005A href=\"%s\"\006%s\005/A\006" uri id
+ in
+ print ch id'
let handle_full_sym ch s uri desc =
let uri = try HExtlib.unopt uri
- with Failure _ -> "cic:/fakeuri.def(1)"
- in print ch "<A title=\"%s\" href=\"%s\">%s</A>" desc uri s
+ with Failure _ -> "cic:/fakeuri.def(1)" in
+ let s' = Printf.sprintf "\005A title=\"%s\" href=\"%s\"\006%s\005/A\006" desc uri s
+ in
+ print ch s'
let handle_full_num ch num uri desc =
let uri = try HExtlib.unopt uri
with Failure _ -> "cic:/fakeuri.def(1)"
- in print ch "<A title=\"%s\" href=\"%s\">%s</A>" desc uri num
+ in
+ let num' = Printf.sprintf "\005A title=\"%s\" href=\"%s\"\006%s\005/A\006" desc uri num
+ in
+ print ch num'
let handle_tex ch s =
(* print "TEX:%s" (remove_left_quote (Ulexing.utf8_lexeme lexbuf)) *)
- print ch "%s" s
+ print ch s
let return_with_loc token begin_cnum end_cnum =
let flocation = HExtlib.floc_of_loc (begin_cnum,end_cnum) in
Ulexing.rollback lexbuf;
k lexbuf
-let handle_interpr loc literal interp outch =
+let handle_interpr loc literal interp outstr =
try
(match DisambiguateTypes.InterprEnv.find loc interp with
| GrafiteAst.Ident_alias (_,uri) ->
- handle_full_id outch literal uri
+ handle_full_id outstr literal uri
| GrafiteAst.Symbol_alias (_,uri,desc) ->
- handle_full_sym outch literal uri desc
+ handle_full_sym outstr literal uri desc
| GrafiteAst.Number_alias (uri,desc) ->
- handle_full_num outch literal uri desc)
- with Not_found -> print outch "%s" literal
+ handle_full_num outstr literal uri desc)
+ with Not_found -> print outstr literal
;;
-let level2_ast_token interp outch =
+let level2_ast_token interp outstr =
let rec aux nesting =
lexer
- | begincom -> (print outch "%s" (Ulexing.utf8_lexeme lexbuf);
+ | begincom -> (print outstr (Ulexing.utf8_lexeme lexbuf);
aux (nesting+1) lexbuf)
- | endcom -> (print outch "%s" (Ulexing.utf8_lexeme lexbuf);
+ | endcom -> (print outstr (Ulexing.utf8_lexeme lexbuf);
aux (max 0 (nesting-1)) lexbuf)
| eof -> return lexbuf ()
| _ -> if nesting > 0
- then (print outch "%s" (Ulexing.utf8_lexeme lexbuf);
+ then (print outstr (Ulexing.utf8_lexeme lexbuf);
aux nesting lexbuf)
else (Ulexing.rollback lexbuf;
basic_lexer lexbuf)
lexer
| ident -> let loc = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
let id = Ulexing.utf8_lexeme lexbuf in
- handle_interpr loc id interp outch;
+ handle_interpr loc id interp outstr;
aux 0 lexbuf
| variable_ident ->
let loc = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
let id = Ulexing.utf8_lexeme lexbuf in
- handle_interpr loc id interp outch;
+ handle_interpr loc id interp outstr;
aux 0 lexbuf
| pident -> let loc = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
let id = Ulexing.utf8_lexeme lexbuf in
- handle_interpr loc id interp outch;
+ handle_interpr loc id interp outstr;
aux 0 lexbuf
| number ->
let loc = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
let num = Ulexing.utf8_lexeme lexbuf in
- handle_interpr loc num interp outch;
+ handle_interpr loc num interp outstr;
aux 0 lexbuf
| tex_token ->
let loc = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
let s = Ulexing.utf8_lexeme lexbuf in
- handle_interpr loc s interp outch;
+ handle_interpr loc s interp outstr;
aux 0 lexbuf
- | qstring -> (print outch "%s" (Ulexing.utf8_lexeme lexbuf); aux 0 lexbuf)
+ | qstring -> (print outstr (Ulexing.utf8_lexeme lexbuf); aux 0 lexbuf)
| csymbol ->
let loc = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
let s = Ulexing.utf8_lexeme lexbuf in
- handle_interpr loc s interp outch;
+ handle_interpr loc s interp outstr;
aux 0 lexbuf
| eof -> return lexbuf ()
| _ ->
let loc = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
let s = Ulexing.utf8_lexeme lexbuf in
- handle_interpr loc s interp outch;
+ handle_interpr loc s interp outstr;
aux 0 lexbuf
in aux 0
(*let status =
List.fold_right StringSet.add (initial_keywords @ keywords) StringSet.empty
in*)
- mk_lexer (level2_ast_token outch interpr)
+ mk_lexer (level2_ast_token outstr interpr)
;;*)
-let mk_small_printer interpr outch =
+let mk_small_printer interpr outstr =
let initial_keywords =
[ "CProp"; "Prop"; "Type"; "Set"; "let"; "match";
"with"; "in"; "and"; "to"; "as"; "on"; "return"; "done";
(* let status =
List.fold_right StringSet.add initial_keywords StringSet.empty
in *)
- level2_ast_token interpr outch
+ level2_ast_token interpr outstr
;;
(* let mk_small_lexer interpr = mk_small_lexer interpr [];;*)