X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FsmallLexer.ml;h=c61fb9cc8e716fe70f59b2531f245125a0de20eb;hb=dee464f8cd331524663167659d1fad01e558d4e1;hp=7e850dfe708a7f27a1bda6031bcb5db081776016;hpb=d83fa3d6e3604bcc596840219f3998d795630d66;p=helm.git
diff --git a/matitaB/components/content_pres/smallLexer.ml b/matitaB/components/content_pres/smallLexer.ml
index 7e850dfe7..c61fb9cc8 100644
--- a/matitaB/components/content_pres/smallLexer.ml
+++ b/matitaB/components/content_pres/smallLexer.ml
@@ -132,24 +132,34 @@ let expand_macro 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)
-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 "%s" 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 "%s" 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 "%s" 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
@@ -175,28 +185,28 @@ let ligatures_token k =
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)
@@ -204,38 +214,38 @@ let level2_ast_token interp outch =
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
@@ -251,10 +261,10 @@ let level2_ast_token interp outch =
(*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";
@@ -263,7 +273,7 @@ let mk_small_printer interpr outch =
(* 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 [];;*)