1) Matitaweb now disambiguates scripts as it runs them

[helm.git] / matitaB / components / content_pres / smallLexer.ml

diff --git a/matitaB/components/content_pres/smallLexer.ml b/matitaB/components/content_pres/smallLexer.ml
index 7e850dfe708a7f27a1bda6031bcb5db081776016..c61fb9cc8e716fe70f59b2531f245125a0de20eb 100644 (file)
--- 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 "<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
@@ -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 [];;*)