renderingAttrs.cmi:
cicNotationLexer.cmi:
+interpTable.cmi:
+smallLexer.cmi:
cicNotationParser.cmi:
mpresentation.cmi:
box.cmi:
renderingAttrs.cmx: renderingAttrs.cmi
cicNotationLexer.cmo: cicNotationLexer.cmi
cicNotationLexer.cmx: cicNotationLexer.cmi
+interpTable.cmo: interpTable.cmi
+interpTable.cmx: interpTable.cmi
+smallLexer.cmo: smallLexer.cmi
+smallLexer.cmx: smallLexer.cmi
cicNotationParser.cmo: cicNotationLexer.cmi cicNotationParser.cmi
cicNotationParser.cmx: cicNotationLexer.cmx cicNotationParser.cmi
mpresentation.cmo: mpresentation.cmi
("(" number (',' number)* ")")? (* reference spec *)
let regexp qstring = '"' [^ '"']* '"'
-let regexp hreftag = "<A"
+let regexp hreftag = "<" [ 'A' 'a' ]
let regexp href = "href=\"" uri "\""
let regexp hreftitle = "title=" qstring
-let regexp hrefclose = "</A>"
+let regexp hrefclose = "</" [ 'A' 'a' ] ">"
let regexp tex_token = '\\' ident
| [] -> None
| (ctx0,t0 as hd)::tl ->
(* prerr_endline ("ok! length tl = " ^ string_of_int (List.length tl)); *)
- prerr_endline ("visiting t0 = " ^ pp_term t0);
- if test t0 then (prerr_endline "t0 is ambiguous"; Some hd)
+ debug_print (lazy ("visiting t0 = " ^ pp_term t0));
+ if test t0 then (debug_print (lazy "t0 is ambiguous"); Some hd)
else
(*
(prerr_endline ("splitting not ambiguous t0:");
in match (refine_profiler.HExtlib.profile foo ()) with
| Ko x ->
let _,err = Lazy.force x in
- prerr_endline ("test_interpr error: " ^ err);
+ debug_print (lazy ("test_interpr error: " ^ err));
false
| _ -> true
with
let res =
Environment.find item universe
in
- prerr_endline (Printf.sprintf "choices for %s :\n%s"
- (d2s item) (String.concat ", " (List.map a2s res)));
+ debug_print (lazy (Printf.sprintf "choices for %s :\n%s"
+ (d2s item) (String.concat ", " (List.map a2s res))));
res
in
match ts with
| [] -> None
| t0 :: tl ->
- prerr_endline ("disambiguate_list: t0 = " ^ pp_thing t0);
+ debug_print (lazy ("disambiguate_list: t0 = " ^ pp_thing t0));
let is_ambiguous = function
| Ast.Ident (_,`Ambiguous)
| Ast.Num (_,None)
(* get first ambiguous subterm (or return disambiguated term) *)
match visit ~pp_term is_ambiguous t0 with
| None ->
- prerr_endline ("visit -- not ambiguous node:\n" ^ pp_thing t0);
+ debug_print (lazy ("visit -- not ambiguous node:\n" ^ pp_thing t0));
Some (t0,tl)
| Some (ctx, t) ->
- prerr_endline ("visit -- found ambiguous node: " ^ astpp t ^
- "\nin " ^ pp_thing (ctx t));
+ debug_print (lazy ("visit -- found ambiguous node: " ^ astpp t ^
+ "\nin " ^ pp_thing (ctx t)));
(* get possible instantiations of t *)
let instances = get_instances ctx t in
- prerr_endline ("-- possible instances:");
+ debug_print (lazy "-- possible instances:");
List.iter
- (fun u0 -> prerr_endline ("-- instance: " ^ (pp_thing u0))) instances;
+ (fun u0 -> debug_print (lazy ("-- instance: " ^ (pp_thing u0)))) instances;
(* perforate ambiguous subterms and test refinement *)
- prerr_endline ("-- survivors:");
+ debug_print (lazy "-- survivors:");
let survivors = List.filter test_interpr instances in
List.iter
- (fun u0 -> prerr_endline ("-- survivor: " ^ (pp_thing u0))) survivors;
+ (fun u0 -> debug_print (lazy ("-- survivor: " ^ (pp_thing u0)))) survivors;
disambiguate_list (survivors@tl)
;;
let refine t =
let localization_tbl = mk_localization_tbl 503 in
- prerr_endline "before interpretate_thing";
+ debug_print (lazy "before interpretate_thing");
let t' =
interpretate_thing ~context ~env ~universe ~uri ~is_path:false t ~localization_tbl
in
- prerr_endline "after interpretate_thing";
+ debug_print (lazy "after interpretate_thing");
match refine_thing metasenv subst context uri ~use_coercions t' expty
base_univ ~localization_tbl with
| Ok (t',m',s',u') -> t,m',s',t',u'
| Uncertain x ->
let _,err = Lazy.force x in
- prerr_endline ("refinement uncertain after disambiguation: " ^ err);
+ debug_print (lazy ("refinement uncertain after disambiguation: " ^ err));
assert false
| _ -> assert false
in
if not (test_interpr thing) then
- (prerr_endline ("preliminary test fail: " ^ pp_thing thing);
+ (debug_print (lazy ("preliminary test fail: " ^ pp_thing thing));
raise (NoWellTypedInterpretation (0,[])))
else
let res = aux [thing] in
let res =
HExtlib.filter_map (fun t ->
try Some (refine t)
- with _ -> prerr_endline ("can't interpretate/refine " ^ (pp_thing t));None) res
+ with _ ->
+ debug_print (lazy ("can't interpretate/refine " ^ (pp_thing t)));None) res
in
match res with
| [] -> raise (NoWellTypedInterpretation (0,[]))
assert (not (List.mem tag !already_registered));
already_registered := tag :: !already_registered;
let old_require1 = !require1 in
+ prerr_endline "let old_require 1 superata";
require1 :=
(fun ~alias_only ((tag',data) as x) ->
if tag=tag' then
+ (prerr_endline ("requiring tag': " ^ tag');
require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term
- ~refresh_uri_in_reference ~alias_only
+ ~refresh_uri_in_reference ~alias_only)
else
old_require1 ~alias_only x);
+ prerr_endline ("added require tag" ^ tag);
(fun x -> tag,Obj.repr x)
end
matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi
matitac.cmo: matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaEngine.cmi
matitac.cmx: matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaEngine.cmx
-matitaEngine.cmo: matitaEngine.cmi
-matitaEngine.cmx: matitaEngine.cmi
+matitadaemon.cmo: matitaInit.cmi matitaGtkMisc.cmi matitaEngine.cmi
+matitadaemon.cmx: matitaInit.cmx matitaGtkMisc.cmx matitaEngine.cmx
+matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi
+matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi
matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi
matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi
matitaGeneratedGui.cmo:
matitaGtkMisc.cmx: matitaTypes.cmx matitaGeneratedGui.cmx buildTimeConf.cmx \
matitaGtkMisc.cmi
matitaGui.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \
- matitaMathView.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmo \
- matitaExcPp.cmi buildTimeConf.cmo matitaGui.cmi
+ matitaMathView.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi \
+ matitaGeneratedGui.cmo matitaExcPp.cmi buildTimeConf.cmo matitaGui.cmi
matitaGui.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
- matitaMathView.cmx matitaGtkMisc.cmx matitaGeneratedGui.cmx \
- matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi
+ matitaMathView.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx \
+ matitaGeneratedGui.cmx matitaExcPp.cmx buildTimeConf.cmx matitaGui.cmi
matitaInit.cmo: matitaExcPp.cmi buildTimeConf.cmo matitaInit.cmi
matitaInit.cmx: matitaExcPp.cmx buildTimeConf.cmx matitaInit.cmi
matitaMathView.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
- matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \
- cicMathView.cmi buildTimeConf.cmo applyTransformation.cmi \
- matitaMathView.cmi
+ matitaGuiTypes.cmi matitaGtkMisc.cmi matitaGeneratedGui.cmo \
+ matitaExcPp.cmi lablGraphviz.cmi cicMathView.cmi buildTimeConf.cmo \
+ applyTransformation.cmi matitaMathView.cmi
matitaMathView.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
- matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx lablGraphviz.cmx \
- cicMathView.cmx buildTimeConf.cmx applyTransformation.cmx \
- matitaMathView.cmi
+ matitaGuiTypes.cmi matitaGtkMisc.cmx matitaGeneratedGui.cmx \
+ matitaExcPp.cmx lablGraphviz.cmx cicMathView.cmx buildTimeConf.cmx \
+ applyTransformation.cmx matitaMathView.cmi
matitaMisc.cmo: matitaGuiTypes.cmi buildTimeConf.cmo matitaMisc.cmi
matitaMisc.cmx: matitaGuiTypes.cmi buildTimeConf.cmx matitaMisc.cmi
matita.cmo: predefined_virtuals.cmi matitaScript.cmi matitaInit.cmi \
- matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmo
+ matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmo applyTransformation.cmi
matita.cmx: predefined_virtuals.cmx matitaScript.cmx matitaInit.cmx \
- matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx
-matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaMisc.cmi \
- matitaMathView.cmi matitaGtkMisc.cmi matitaEngine.cmi cicMathView.cmi \
- buildTimeConf.cmo matitaScript.cmi
-matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaMisc.cmx \
- matitaMathView.cmx matitaGtkMisc.cmx matitaEngine.cmx cicMathView.cmx \
- buildTimeConf.cmx matitaScript.cmi
+ matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx applyTransformation.cmx
+matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaScriptLexer.cmi \
+ matitaMisc.cmi matitaMathView.cmi matitaGtkMisc.cmi matitaEngine.cmi \
+ cicMathView.cmi buildTimeConf.cmo matitaScript.cmi
+matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaScriptLexer.cmx \
+ matitaMisc.cmx matitaMathView.cmx matitaGtkMisc.cmx matitaEngine.cmx \
+ cicMathView.cmx buildTimeConf.cmx matitaScript.cmi
matitaTypes.cmo: matitaTypes.cmi
matitaTypes.cmx: matitaTypes.cmi
predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi
cicMathView.cmi: matitaGuiTypes.cmi applyTransformation.cmi
lablGraphviz.cmi:
matitaclean.cmi:
-matitaEngine.cmi:
+matitaEngine.cmi: applyTransformation.cmi
matitaExcPp.cmi:
matitaGtkMisc.cmi: matitaGeneratedGui.cmo
matitaGui.cmi: matitaGuiTypes.cmi
-matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmo \
- applyTransformation.cmi
+matitaGuiTypes.cmi: matitaGeneratedGui.cmo applyTransformation.cmi
matitaInit.cmi:
matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi
matitaMisc.cmi: matitaGuiTypes.cmi
+matitaScriptLexer.cmi:
matitaScript.cmi:
matitaTypes.cmi:
predefined_virtuals.cmi:
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+(* $Id: cicNotationLexer.ml 11231 2011-03-30 11:52:27Z ricciott $ *)
+
+open Printf
+
+exception Error of int * int * string
+
+module StringSet = Set.Make(String)
+
+(* Lexer *)
+let regexp number = xml_digit+
+let regexp utf8_blank = " " | "\r\n" | "\n" | "\t" | [160] (* this is a nbsp *)
+let regexp percentage =
+ ('-' | "") [ '0' - '9' ] + '%'
+let regexp floatwithunit =
+ ('-' | "") [ '0' - '9' ] + ["."] [ '0' - '9' ] + ([ 'a' - 'z' ] + | "" )
+let regexp color = "#" [ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f'
+'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ]
+[ '0' - '9' 'a' - 'f' 'A' - 'F' ] [ '0' - '9' 'a' - 'f' 'A' - 'F' ]
+
+ (* ZACK: breaks unicode's binder followed by an ascii letter without blank *)
+(* let regexp ident_letter = xml_letter *)
+
+let regexp ident_letter = [ 'a' - 'z' 'A' - 'Z' ]
+
+ (* must be in sync with "is_ligature_char" below *)
+let regexp ligature_char = [ "'`~!?@*()[]<>-+=|:;.,/\"" ]
+let regexp ligature = ligature_char ligature_char+
+
+let regexp we_proved = "we" utf8_blank+ "proved"
+let regexp we_have = "we" utf8_blank+ "have"
+let regexp let_rec = "let" utf8_blank+ "rec"
+let regexp let_corec = "let" utf8_blank+ "corec"
+let regexp ident_decoration = '\'' | '?' | '`'
+let regexp ident_cont = ident_letter | xml_digit | '_'
+let regexp ident_start = ident_letter
+let regexp ident = ident_letter ident_cont* ident_decoration*
+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 hreftag = "<" [ 'A' 'a' ]
+let regexp href = "href=\"" uri "\""
+let regexp hreftitle = "title=" qstring
+let regexp hrefclose = "</" [ 'A' 'a' ] ">"
+
+let regexp tex_token = '\\' ident
+
+let regexp delim_begin = "\\["
+let regexp delim_end = "\\]"
+
+let regexp qkeyword = "'" ( ident | pident ) "'"
+
+let regexp implicit = '?'
+let regexp placeholder = '%'
+let regexp meta = implicit number
+
+let regexp csymbol = '\'' ident
+
+let regexp begin_group = "@{" | "${"
+let regexp end_group = '}'
+let regexp wildcard = "$_"
+let regexp ast_ident = "@" ident
+let regexp ast_csymbol = "@" csymbol
+let regexp meta_ident = "$" ident
+let regexp meta_anonymous = "$_"
+
+let regexp begincom = "(*"
+let regexp endcom = "*)"
+(* let regexp comment_char = [^'*'] | '*'[^')']
+let regexp note = "|+" ([^'*'] | "**") comment_char* "+|" *)
+
+let level1_layouts =
+ [ "sub"; "sup";
+ "below"; "above";
+ "over"; "atop"; "frac";
+ "sqrt"; "root"; "mstyle" ; "mpadded"; "maction"
+
+ ]
+
+let level1_keywords =
+ [ "hbox"; "hvbox"; "hovbox"; "vbox";
+ "break";
+ "list0"; "list1"; "sep";
+ "opt";
+ "term"; "ident"; "number";
+ ] @ level1_layouts
+
+let level2_meta_keywords =
+ [ "if"; "then"; "elCicNotationParser.se";
+ "fold"; "left"; "right"; "rec";
+ "fail";
+ "default";
+ "anonymous"; "ident"; "number"; "term"; "fresh"
+ ]
+
+ (* (string, int) Hashtbl.t, with multiple bindings.
+ * int is the unicode codepoint *)
+let ligatures = Hashtbl.create 23
+
+let _ =
+ List.iter
+ (fun (ligature, symbol) -> Hashtbl.add ligatures ligature symbol)
+ [ ("->", <:unicode<to>>); ("=>", <:unicode<Rightarrow>>);
+ (":=", <:unicode<def>>);
+ ]
+
+let regexp nreference =
+ "cic:/" (* schema *)
+ uri_step ('/' uri_step)* (* path *)
+ '.'
+ ( "dec"
+ | "def" "(" number ")"
+ | "fix" "(" number "," number "," number ")"
+ | "cfx" "(" number ")"
+ | "ind" "(" number "," number "," number ")"
+ | "con" "(" number "," number "," number ")") (* ext + reference *)
+
+let error lexbuf msg =
+ let begin_cnum, end_cnum = Ulexing.loc lexbuf in
+ raise (Error (begin_cnum, end_cnum, msg))
+let error_at_end lexbuf msg =
+ 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 return lexbuf token =
+ let begin_cnum, end_cnum = Ulexing.loc lexbuf in
+ return_with_loc token begin_cnum end_cnum
+
+let return_lexeme lexbuf name = return lexbuf (name, Ulexing.utf8_lexeme lexbuf)
+
+let return_symbol lexbuf s = return lexbuf ("SYMBOL", s)
+let return_eoi lexbuf = return lexbuf ("EOI", "")
+
+let remove_quotes s = String.sub s 1 (String.length s - 2)
+
+let mk_lexer token =
+ let tok_func stream =
+(* let lexbuf = Ulexing.from_utf8_stream stream in *)
+(** XXX Obj.magic rationale.
+ * The problem.
+ * camlp5 constraints the tok_func field of Token.glexer to have type:
+ * Stream.t char -> (Stream.t 'te * flocation_function)
+ * In order to use ulex we have (in theory) to instantiate a new lexbuf each
+ * time a char Stream.t is passed, destroying the previous lexbuf which may
+ * have consumed a character from the old stream which is lost forever :-(
+ * The "solution".
+ * Instead of passing to camlp5 a char Stream.t we pass a lexbuf, casting it to
+ * char Stream.t with Obj.magic where needed.
+ *)
+ let lexbuf = Obj.magic stream in
+ Token.make_stream_and_location
+ (fun () ->
+ try
+ token lexbuf
+ with
+ | Ulexing.Error -> error_at_end lexbuf "Unexpected character"
+ | Ulexing.InvalidCodepoint p ->
+ error_at_end lexbuf (sprintf "Invalid code point: %d" p))
+ in
+ {
+ Token.tok_func = tok_func;
+ Token.tok_using = (fun _ -> ());
+ Token.tok_removing = (fun _ -> ());
+ Token.tok_match = Token.default_match;
+ Token.tok_text = Token.lexer_text;
+ Token.tok_comm = None;
+ }
+
+let expand_macro lexbuf =
+ let macro =
+ Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1)
+ in
+ try
+ ("SYMBOL", Utf8Macro.expand macro)
+ with Utf8Macro.Macro_not_found _ ->
+(* FG: unexpanded TeX macros are terminated by a space for rendering *)
+ "SYMBOL", (Ulexing.utf8_lexeme 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 rec level2_pattern_token_group counter buffer =
+ lexer
+ | end_group ->
+ if (counter > 0) then
+ Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ;
+ snd (Ulexing.loc lexbuf)
+ | begin_group ->
+ Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ;
+ ignore (level2_pattern_token_group (counter + 1) buffer lexbuf) ;
+ level2_pattern_token_group counter buffer lexbuf
+ | _ ->
+ Buffer.add_string buffer (Ulexing.utf8_lexeme lexbuf) ;
+ level2_pattern_token_group counter buffer lexbuf
+
+let read_unparsed_group token_name lexbuf =
+ let buffer = Buffer.create 16 in
+ let begin_cnum, _ = Ulexing.loc lexbuf in
+ let end_cnum = level2_pattern_token_group 0 buffer lexbuf in
+ return_with_loc (token_name, Buffer.contents buffer) begin_cnum end_cnum
+
+let handle_keywords lexbuf k name =
+ let s = Ulexing.utf8_lexeme lexbuf in
+ if k s then
+ return lexbuf ("", s)
+ else
+ return lexbuf (name, s)
+;;
+
+let rec level2_meta_token =
+ lexer
+ | utf8_blank+ -> level2_meta_token lexbuf
+ | hreftag -> return lexbuf ("ATAG","")
+ | hrefclose -> return lexbuf ("ATAGEND","")
+ | ident ->
+ handle_keywords lexbuf (fun x -> List.mem x level2_meta_keywords) "IDENT"
+ | variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
+ | pident ->
+ handle_keywords lexbuf (fun x -> List.mem x level2_meta_keywords) "PIDENT"
+ | "@{" -> read_unparsed_group "UNPARSED_AST" lexbuf
+ | ast_ident ->
+ return lexbuf ("UNPARSED_AST",
+ remove_left_quote (Ulexing.utf8_lexeme lexbuf))
+ | ast_csymbol ->
+ return lexbuf ("UNPARSED_AST",
+ remove_left_quote (Ulexing.utf8_lexeme lexbuf))
+ | eof -> return_eoi lexbuf
+
+
+ (** @param k continuation to be invoked when no ligature has been found *)
+let ligatures_token k =
+ lexer
+ | ligature ->
+ let lexeme = Ulexing.utf8_lexeme lexbuf in
+ (match List.rev (Hashtbl.find_all ligatures lexeme) with
+ | [] -> (* ligature not found, rollback and try default lexer *)
+ Ulexing.rollback lexbuf;
+ k lexbuf
+ | default_lig :: _ -> (* ligatures found, use the default one *)
+ return_symbol lexbuf default_lig)
+ | eof -> return_eoi lexbuf
+ | _ -> (* not a ligature, rollback and try default lexer *)
+ Ulexing.rollback lexbuf;
+ k lexbuf
+
+
+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));
+ CicNotationLexer.LocalizeEnv.add loc (href,desc) loctable)
+ else loctable
+;; *)
+
+let get_hot_spots =
+
+ (* k = lexing continuation *)
+ let rec aux nesting k =
+ lexer
+ | begincom -> aux (nesting+1) k lexbuf
+ | endcom -> aux (max 0 (nesting-1)) k lexbuf
+ | eof -> []
+ | _ -> if nesting > 0
+ then aux nesting k lexbuf
+ else (Ulexing.rollback lexbuf;
+ k lexbuf)
+ and aux_basic loc1 desc href =
+ lexer
+ | hreftag -> aux 0 (aux_in_tag (Ulexing.loc lexbuf) None None) lexbuf
+ | hrefclose ->
+ (try
+ let loc1 = HExtlib.floc_of_loc (HExtlib.unopt loc1) in
+ let loc2 = HExtlib.floc_of_loc (Ulexing.loc lexbuf) in
+ (loc1,loc2,href,desc) :: aux 0 (aux_basic None None None) lexbuf
+ with Failure _ -> aux 0 (aux_basic None None None) lexbuf)
+ | eof -> []
+ | _ -> aux 0 (aux_basic loc1 desc href) lexbuf
+ and aux_in_tag loc1 desc href = lexer
+ | utf8_blank+ -> aux 0 (aux_in_tag loc1 desc href) lexbuf
+ | href ->
+ aux 0 (aux_in_tag loc1 desc (Some (Ulexing.utf8_sub_lexeme
+ lexbuf 6 (Ulexing.lexeme_length lexbuf - 7))))
+ lexbuf
+ | hreftitle ->
+ aux 0 (aux_in_tag loc1 (Some (Ulexing.utf8_sub_lexeme lexbuf 7
+ (Ulexing.lexeme_length lexbuf - 8))) href)
+ lexbuf
+ | ">" ->
+ let merge (a,b) (c,d) = (a,d) in
+ aux 0
+ (aux_basic (Some (merge loc1 (Ulexing.loc lexbuf))) desc href) lexbuf
+ | _ -> aux 0 (aux_basic None None None) lexbuf
+ in aux 0 (aux_basic None None None)
+
+let get_hot_spots s = get_hot_spots (Ulexing.from_utf8_string s)
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+ (** begin of error offset (counted in unicode codepoint)
+ * end of error offset (counted as above)
+ * error message *)
+exception Error of int * int * string
+
+val get_hot_spots : string ->
+ (Stdpp.location * Stdpp.location * string option * string option) list
+
+
--- /dev/null
+open Printf;;
+open Http_types;;
+
+(*** from matitaScript.ml ***)
+(* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *)
+
+let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script *)
+ statement
+=
+ let ast,unparsed_text =
+ match statement with
+ | `Raw text ->
+ (* if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; *)
+ let strm =
+ GrafiteParser.parsable_statement status
+ (Ulexing.from_utf8_string text) in
+ let ast = MatitaEngine.get_ast status include_paths strm in
+ ast, text
+ | `Ast (st, text) -> st, text
+ in
+ let floc = match ast with
+ | GrafiteAst.Executable (loc, _)
+ | GrafiteAst.Comment (loc, _) -> loc in
+
+ let _,lend = HExtlib.loc_of_floc floc in
+ let parsed_text, parsed_text_len =
+ MatitaGtkMisc.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in
+
+ let status =
+ MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
+ in
+ (status, parsed_text),"",(*parsed_text_len*) Glib.Utf8.length parsed_text
+
+
+let status = ref (new MatitaEngine.status "cic:/matita");;
+
+let include_paths = ["/home/barolo/matitaB/matita/lib"];;
+
+let advance text (* (?bos=false) *) =
+ (* if bos then LibraryClean.clean_baseuris [self#buri_of_current_file];
+ (* HLog.debug ("evaluating: " ^ first_line s ^ " ...");*)
+ let time1 = Unix.gettimeofday () in
+ let entries, newtext, parsed_len = *)
+ let (st,_),_,parsed_len =
+ (* try *)
+ eval_statement include_paths (*buffer*) !status (`Raw text)
+ (* with End_of_file -> raise Margin *)
+ in
+ status := st;
+ let _,_,metasenv,subst,_ = !status#obj in
+ let txt = List.fold_left
+ (fun acc (nmeta,_ as meta) ->
+ let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 ()
+ (snd (ApplyTransformation.ntxt_of_cic_sequent
+ ~metasenv ~subst ~map_unicode_to_tex:false 80 !status meta)) in
+ ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
+ [] metasenv
+ in
+ let txt = String.concat "\n\n" txt in
+ parsed_len, txt
+ (*in
+ let time2 = Unix.gettimeofday () in
+ HLog.debug ("... done in " ^ string_of_float (time2 -. time1) ^ "s");
+ let new_statuses, new_statements =
+ let statuses, texts = List.split entries in
+ statuses, texts
+ in
+ history <- new_statuses @ history;
+ statements <- new_statements @ statements;
+ let start = buffer#get_iter_at_mark (`MARK locked_mark) in
+ let new_text = String.concat "" (List.rev new_statements) in
+ if statement <> None then
+ buffer#insert ~iter:start new_text
+ else begin
+ let parsed_text = String.sub s 0 parsed_len in
+ if new_text <> parsed_text then begin
+ let stop = start#copy#forward_chars (Glib.Utf8.length parsed_text) in
+ buffer#delete ~start ~stop;
+ buffer#insert ~iter:start new_text;
+ end;
+ end;
+ self#moveMark (Glib.Utf8.length new_text);
+ buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext*)
+;;
+
+let read_file fname =
+ let chan = open_in fname in
+ let lines = ref [] in
+ (try
+ while true do
+ lines := input_line chan :: !lines
+ done;
+ with End_of_file -> close_in chan);
+ String.concat "\r\n" (List.rev !lines)
+;;
+
+let load_index outchan =
+ let s = read_file "index.html" in
+ Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
+;;
+
+let call_service outchan =
+ try
+ (ignore(MatitaEngine.assert_ng
+ ~include_paths:["/home/barolo/matitaB/matita/lib"] (* ~outch:outchan *)
+ "/home/barolo/matitaB/matita/lib/basics/pts.ma");
+ prerr_endline "fatto";
+ let s = read_file "/home/barolo/matitaB/matita/lib/basics/pts.ma.mad"
+ in
+ Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
+ )
+ with
+ e -> Http_daemon.respond ~code:(`Code 500) outchan
+;;
+
+let callback req outchan =
+ let str =
+ (sprintf "request path = %s\n" req#path) ^
+ (sprintf "request GET params = %s\n"
+ (String.concat ";"
+ (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_GET))) ^
+ (sprintf "request POST params = %s\n"
+ (String.concat ";"
+ (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params_POST))) ^
+ (sprintf "request ALL params = %s\n"
+ (String.concat ";"
+ (List.map (fun (h,v) -> String.concat "=" [h;v]) req#params))) ^
+ (sprintf "cookies = %s\n"
+ (match req#cookies with
+ | None ->
+ "NO COOKIES "
+ ^ (if req#hasHeader ~name:"cookie"
+ then "('Cookie:' header was '" ^ req#header ~name:"cookie" ^ "')"
+ else "(No 'Cookie:' header received)")
+ | Some cookies ->
+ (String.concat ";"
+ (List.map (fun (n,v) -> String.concat "=" [n;v]) cookies)))) ^
+ (sprintf "request BODY = '%s'\n\n" req#body)
+ in
+ (* Http_daemon.respond ~code:(`Code 200) ~body: str outchan *)
+
+ prerr_endline str;
+
+ match req#path with
+ | "/" -> load_index outchan
+ | "/matita" -> call_service outchan
+ | "/open" ->
+ prerr_endline "getting 'file' argument";
+ let filename = List.assoc "file" req#params_GET in
+ prerr_endline ("reading file " ^ filename);
+ let body = read_file filename in
+ let _,baseuri,_,_ =
+ Librarian.baseuri_of_script ~include_paths:[] filename
+ in
+ status := (!status)#set_baseuri baseuri;
+ Http_daemon.respond ~code:(`Code 200) ~body outchan
+ | "/advance" ->
+ let script = req#body in
+ prerr_endline ("body length = " ^ (string_of_int (String.length script)));
+ let (parsed_len,txt), res, code =
+ try advance script, "OK", `Code 200
+ with
+ | HExtlib.Localized(_,e)
+ | e ->
+ (prerr_endline ("exception: " ^ Printexc.to_string e);
+ (try
+ NTacStatus.pp_tac_status !status
+ with e -> prerr_endline ("inner exception: " ^
+ Printexc.to_string e));
+ prerr_endline "end status";
+ let _,_,metasenv,subst,_ = !status#obj in
+ let txt = List.fold_left
+ (fun acc (nmeta,_ as meta) ->
+ let txt0 = Netencoding.Html.encode ~in_enc:`Enc_utf8 ()
+ (snd (ApplyTransformation.ntxt_of_cic_sequent
+ ~metasenv ~subst ~map_unicode_to_tex:false 80 !status meta)) in
+ ("<B>Goal ?" ^ (string_of_int nmeta) ^ "</B>\n" ^ txt0)::acc)
+ [] metasenv
+ in
+ let txt = String.concat "\n\n" txt in
+ (0,txt), Printexc.to_string e, `Code 500)
+ in
+ let txt = Netencoding.Url.encode ~plus:false txt in
+ let body = (string_of_int parsed_len) ^ "#" ^ txt in
+ Http_daemon.respond ~code ~body outchan
+ | url -> Http_daemon.respond_not_found ~url outchan
+
+;;
+
+
+
+let spec =
+ { Http_daemon.default_spec with
+ callback = callback;
+ port = 9999;
+ mode = `Single;
+ }
+;;
+
+let _ =
+ MatitaInit.initialize_all ();
+ Http_daemon.main spec
+;;
projects / helm.git / commitdiff