From: Wilmer Ricciotti Date: Wed, 20 Jul 2011 15:34:52 +0000 (+0000) Subject: 1) Matitaweb now disambiguates scripts as it runs them X-Git-Tag: make_still_working~2358 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=dee464f8cd331524663167659d1fad01e558d4e1 1) Matitaweb now disambiguates scripts as it runs them 2) Fixed bugs in HTML escaping (also changed the syntax of annotations in matita scripts) --- diff --git a/matitaB/components/METAS/meta.helm-syntax_extensions.src b/matitaB/components/METAS/meta.helm-syntax_extensions.src index f9e210f6e..5d3c8734d 100644 --- a/matitaB/components/METAS/meta.helm-syntax_extensions.src +++ b/matitaB/components/METAS/meta.helm-syntax_extensions.src @@ -1,4 +1,4 @@ -requires="str" +requires="str netstring" version="0.0.1" archive(byte)="utf8_macros.cma" archive(native)="utf8_macros.cmxa" diff --git a/matitaB/components/content_pres/cicNotationLexer.ml b/matitaB/components/content_pres/cicNotationLexer.ml index ce8fcec54..f5e8ba010 100644 --- a/matitaB/components/content_pres/cicNotationLexer.ml +++ b/matitaB/components/content_pres/cicNotationLexer.ml @@ -73,10 +73,21 @@ let regexp uri = ("(" number (',' number)* ")")? (* reference spec *) let regexp qstring = '"' [^ '"']* '"' -let regexp hreftag = "<" [ 'A' 'a' ] +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 = "" +let regexp hrefclose = xmarkup "/" [ 'A' 'a' ] ymarkup + +let regexp tag_cont = ident_letter | xml_digit | "_" | "-" +let regexp tagname = ident_letter tag_cont* +let regexp opentag = xmarkup tagname +let regexp closetag = xmarkup "/" tagname ymarkup +let regexp attribute = tagname "=" qstring +let regexp generictag = + opentag (utf8_blank+ attribute)* ymarkup let regexp tex_token = '\\' ident @@ -255,6 +266,8 @@ let rec level2_meta_token = | 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) @@ -337,6 +350,8 @@ let level2_ast_token loctable status = | placeholder -> return lexbuf ("PLACEHOLDER", "") | hreftag -> aux_in_tag None None lexbuf | hrefclose -> aux None None lexbuf + | generictag + | closetag -> ligatures_token (aux desc href) lexbuf | ident -> loctable := update_table (loc_of_buf lexbuf) desc href !loctable; handle_keywords lexbuf (fun x -> StringSet.mem x status) "IDENT" @@ -399,6 +414,8 @@ let rec level1_pattern_token = | number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf) | 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" diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml index 627291880..8043d73a3 100644 --- a/matitaB/components/content_pres/cicNotationParser.ml +++ b/matitaB/components/content_pres/cicNotationParser.ml @@ -103,7 +103,7 @@ let add_symbol_to_grammar_explicit level2_ast_grammar (Gramext.action (fun _ loc -> None, loc)) ; [Gramext.Stoken ("ATAG","") ;Gramext.Snterm (Grammar.Entry.obj sym_attributes) - ;Gramext.Stoken ("SYMBOL",">") + ;Gramext.Stoken ("SYMBOL","\005") ;Gramext.Stoken ("SYMBOL",s) ;Gramext.Stoken ("ATAGEND","")], (Gramext.action (fun _ uridesc _ _ _ loc -> (Some uridesc),loc)) 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 [];;*) diff --git a/matitaB/components/content_pres/smallLexer.mli b/matitaB/components/content_pres/smallLexer.mli index c4f4565bc..77927a573 100644 --- a/matitaB/components/content_pres/smallLexer.mli +++ b/matitaB/components/content_pres/smallLexer.mli @@ -2,4 +2,4 @@ * unit Token.glexer*) val mk_small_printer : GrafiteAst.alias_spec DisambiguateTypes.InterprEnv.t -> - out_channel -> Ulexing.lexbuf -> unit * Stdpp.location + string ref -> Ulexing.lexbuf -> unit * Stdpp.location diff --git a/matitaB/components/grafite_engine/grafiteEngine.ml b/matitaB/components/grafite_engine/grafiteEngine.ml index 26ba7ffd0..a0b00150f 100644 --- a/matitaB/components/grafite_engine/grafiteEngine.ml +++ b/matitaB/components/grafite_engine/grafiteEngine.ml @@ -771,8 +771,11 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = if dir <> Some `RightToLeft then eval_input_notation status (l1,l2) else status in + let status = if dir <> Some `LeftToRight then eval_output_notation status (l1,l2) else status + in prerr_endline ("new grammar:\n" ^ (Print_grammar.ebnf_of_term status)); + status | GrafiteAst.Alias (loc, spec) -> let diff = (*CSC: Warning: this code should be factorized with the corresponding diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml index 30bd9b834..4b1bdfcc8 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.ml @@ -57,6 +57,9 @@ class virtual status uid = val disambiguate_db = initial_status method disambiguate_db = disambiguate_db method set_disambiguate_db v = {< disambiguate_db = v >} + method reset_disambiguate_db () = + {< disambiguate_db = { self#disambiguate_db with interpr = + DisambiguateTypes.InterprEnv.empty } >} method set_disambiguate_status : 'status. #g_status as 'status -> 'self = fun o -> ((self#set_interp_status o)#set_disambiguate_db o#disambiguate_db) diff --git a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli index b88bc0e1d..fcea29e43 100644 --- a/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli +++ b/matitaB/components/ng_disambiguation/grafiteDisambiguate.mli @@ -37,6 +37,7 @@ class virtual status : inherit g_status inherit Interpretations.status method set_disambiguate_db: db -> 'self + method reset_disambiguate_db: unit -> 'self method set_disambiguate_status: #g_status -> 'self end diff --git a/matitaB/components/syntax_extensions/Makefile b/matitaB/components/syntax_extensions/Makefile index 5f0065d2f..c869ed831 100644 --- a/matitaB/components/syntax_extensions/Makefile +++ b/matitaB/components/syntax_extensions/Makefile @@ -1,6 +1,6 @@ PACKAGE = utf8_macros PREDICATES = -MAKE_TABLE_PACKAGES = helm-xml +MAKE_TABLE_PACKAGES = "netstring helm-xml" # modules which have both a .ml and a .mli INTERFACE_FILES = utf8Macro.mli @@ -15,7 +15,7 @@ make_table: make_table.ml $(H)$(OCAMLFIND) ocamlc -rectypes -package $(MAKE_TABLE_PACKAGES) -linkpkg -o $@ $^ utf8MacroTable.ml: - ./make_table $@ $@.txt + ./make_table $@ $@.txt $(@:%.ml=%.js) utf8MacroTable.cmo: utf8MacroTable.ml @echo " OCAMLC $<" $(H)@$(OCAMLFIND) ocamlc -c $< diff --git a/matitaB/components/syntax_extensions/make_table.ml b/matitaB/components/syntax_extensions/make_table.ml index 59204c6e4..0e9a9ac12 100644 --- a/matitaB/components/syntax_extensions/make_table.ml +++ b/matitaB/components/syntax_extensions/make_table.ml @@ -82,16 +82,26 @@ let parse_from_xml () = let main () = let oc = open_out Sys.argv.(1) in let oc_doc = open_out Sys.argv.(2) in + let oc_js = open_out Sys.argv.(3) in output_string oc "(* GENERATED by make_table: DO NOT EDIT! *)\n"; output_string oc_doc "(* GENERATED by make_table: DO NOT EDIT! *)\n"; + output_string oc_js "/* GENERATED by make_table: DO NOT EDIT! */\n"; output_string oc "let macro2utf8 = Hashtbl.create 2000\n"; output_string oc "let utf82macro = Hashtbl.create 2000\n"; output_string oc "let data = [\n"; + output_string oc_js "var macro2utf8 = new Object();\n"; + output_string oc_js "var utf82macro = new Object();\n"; let macro2utf8 = parse_from_xml () in Hashtbl.iter (fun macro utf8 -> + let hescape s = + String.escaped (Netencoding.Html.encode ~in_enc:`Enc_utf8 () s) in fprintf oc " \"%s\", \"%s\";\n" macro (String.escaped utf8); - fprintf oc_doc "\\%s %s\n" macro utf8) + fprintf oc_doc "\\%s %s\n" macro utf8; + fprintf oc_js "macro2utf8[\"%s\"] = \"%s\";\n" + macro (hescape utf8); + fprintf oc_js "utf82macro[\"%s\"] = \"%s\";\n" + (hescape utf8) macro) macro2utf8; output_string oc " ];;\n"; output_string oc "let _ =\n"; diff --git a/matitaB/components/syntax_extensions/utf8MacroTable.ml b/matitaB/components/syntax_extensions/utf8MacroTable.ml index 588321c48..eefdcea0f 100644 --- a/matitaB/components/syntax_extensions/utf8MacroTable.ml +++ b/matitaB/components/syntax_extensions/utf8MacroTable.ml @@ -2136,5 +2136,5 @@ let _ = List.iter (fun (macro, utf8) -> Hashtbl.replace macro2utf8 macro utf8; - Hashtbl.add utf82macro utf8 macro) + Hashtbl.replace utf82macro utf8 macro) data;; diff --git a/matitaB/matita/Makefile b/matitaB/matita/Makefile index ed24d2c61..9a03d41bf 100644 --- a/matitaB/matita/Makefile +++ b/matitaB/matita/Makefile @@ -61,6 +61,7 @@ CMLI = \ matitaInit.mli \ $(NULL) WMLI = \ + matitaScriptLexer.mli \ matitaTypes.mli \ matitaMisc.mli \ applyTransformation.mli \ diff --git a/matitaB/matita/lib/basics/logic.ma b/matitaB/matita/lib/basics/logic.ma index 34299aff0..374947b7d 100644 --- a/matitaB/matita/lib/basics/logic.ma +++ b/matitaB/matita/lib/basics/logic.ma @@ -20,43 +20,43 @@ inductive eq (A:Type[1]) (x:A) : A → Prop ≝ interpretation "leibnitz's equality" 'eq t x y = (eq t x y). lemma eq_rect_r: - ∀A.∀a,x.∀p:eq ? x a.∀P: - ∀x:A. x = a → Type[2]. P a (refl A a) → P x p. + ∀A.∀a,x.∀p:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A ? x a.∀P: + ∀x:A. x A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A a → Type[2]. P a (refl A a) → P x p. #A #a #x #p (cases p) // qed. lemma eq_ind_r : - ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → - ∀x.∀p:eq ? x a.P x p. - #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed. + ∀A.∀a.∀P: ∀x:A. x A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A a → Prop. P a (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A A a) → + ∀x.∀p:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A ? x a.P x p. + #A #a #P #p #x0 #p0; @(A href="cic:/matita/basics/logic/eq_rect_r.def(1)"eq_rect_r/A ? ? ? p0) //; qed. lemma eq_rect_Type2_r: - ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → - ∀x.∀p:eq ? x a.P x p. + ∀A.∀a.∀P: ∀x:A. A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A ? x a → Type[2]. P a (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A A a) → + ∀x.∀p:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A ? x a.P x p. #A #a #P #H #x #p (generalize in match H) (generalize in match P) cases p; //; qed. -theorem rewrite_l: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. x = y → P y. +theorem rewrite_l: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. x A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A y → P y. #A #x #P #Hx #y #Heq (cases Heq); //; qed. -theorem sym_eq: ∀A.∀x,y:A. x = y → y = x. -#A #x #y #Heq @(rewrite_l A x (λz.z=x)); //; qed. +theorem sym_eq: ∀A.∀x,y:A. x A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A y → y A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A x. +#A #x #y #Heq @(A href="cic:/matita/basics/logic/rewrite_l.def(1)"rewrite_l/A A x (λz.zA title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax)); //; qed. -theorem rewrite_r: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. y = x → P y. -#A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed. +theorem rewrite_r: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. y A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A x → P y. +#A #x #P #Hx #y #Heq (cases (A href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/A ? ? ? Heq)); //; qed. -theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B. +theorem eq_coerc: ∀A,B:Type[0].A→(AA title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/AB)→B. #A #B #Ha #Heq (elim Heq); //; qed. -theorem trans_eq : ∀A.∀x,y,z:A. x = y → y = z → x = z. +theorem trans_eq : ∀A.∀x,y,z:A. x A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A y → y A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A z → x A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A z. #A #x #y #z #H1 #H2 >H1; //; qed. -theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. x=y → f x = f y. +theorem eq_f: ∀A,B.∀f:A→B.∀x,y:A. xA title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ay → f x A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A f y. #A #B #f #x #y #H >H; //; qed. (* deleterio per auto? *) theorem eq_f2: ∀A,B,C.∀f:A→B→C. -∀x1,x2:A.∀y1,y2:B. x1=x2 → y1=y2 → f x1 y1 = f x2 y2. -#A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed. +∀x1,x2:A.∀y1,y2:B. x1A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax2 → y1A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ay2 → f x1 y1 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A f x2 y2. +#A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 E1; E2; //; qed. (* hint to genereric equality definition eq_equality: equality ≝ @@ -80,12 +80,12 @@ inductive False: Prop ≝ . λA. A → False. *) inductive Not (A:Prop): Prop ≝ -nmk: (A → False) → Not A. +nmk: (A → A href="cic:/matita/basics/logic/False.ind(1,0,0)"False/A) → Not A. interpretation "logical not" 'not x = (Not x). -theorem absurd : ∀A:Prop. A → ¬A → False. +theorem absurd : ∀A:Prop. A → A title="logical not" href="cic:/fakeuri.def(1)"¬/AA → A href="cic:/matita/basics/logic/False.ind(1,0,0)"False/A. #A #H #Hn (elim Hn); /2/; qed. (* @@ -93,13 +93,13 @@ ntheorem absurd : ∀ A,C:Prop. A → ¬A → C. #A; #C; #H; #Hn; nelim (Hn H). nqed. *) -theorem not_to_not : ∀A,B:Prop. (A → B) → ¬B →¬A. +theorem not_to_not : ∀A,B:Prop. (A → B) → A title="logical not" href="cic:/fakeuri.def(1)"¬/AB →A title="logical not" href="cic:/fakeuri.def(1)"¬/AA. /4/; qed. (* inequality *) interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)). -theorem sym_not_eq: ∀A.∀x,y:A. x ≠ y → y ≠ x. +theorem sym_not_eq: ∀A.∀x,y:A. x A title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/A y → y A title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/A x. /3/; qed. (* and *) @@ -108,10 +108,10 @@ inductive And (A,B:Prop) : Prop ≝ interpretation "logical and" 'and x y = (And x y). -theorem proj1: ∀A,B:Prop. A ∧ B → A. +theorem proj1: ∀A,B:Prop. A A title="logical and" href="cic:/fakeuri.def(1)"∧/A B → A. #A #B #AB (elim AB) //; qed. -theorem proj2: ∀ A,B:Prop. A ∧ B → B. +theorem proj2: ∀ A,B:Prop. A A title="logical and" href="cic:/fakeuri.def(1)"∧/A B → B. #A #B #AB (elim AB) //; qed. (* or *) @@ -122,7 +122,7 @@ inductive Or (A,B:Prop) : Prop ≝ interpretation "logical or" 'or x y = (Or x y). definition decidable : Prop → Prop ≝ -λ A:Prop. A ∨ ¬ A. +λ A:Prop. A A title="logical or" href="cic:/fakeuri.def(1)"∨/A A title="logical not" href="cic:/fakeuri.def(1)"¬/A A. (* exists *) inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝ @@ -135,7 +135,7 @@ inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝ (* iff *) definition iff := - λ A,B. (A → B) ∧ (B → A). + λ A,B. (A → B) A title="logical and" href="cic:/fakeuri.def(1)"∧/A (B → A). interpretation "iff" 'iff a b = (iff a b). @@ -143,84 +143,84 @@ interpretation "iff" 'iff a b = (iff a b). definition R0 ≝ λT:Type[0].λt:T.t. -definition R1 ≝ eq_rect_Type0. +definition R1 ≝ A href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/A. (* useless stuff *) definition R2 : ∀T0:Type[0]. ∀a0:T0. - ∀T1:∀x0:T0. a0=x0 → Type[0]. - ∀a1:T1 a0 (refl ? a0). - ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0]. - ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1). + ∀T1:∀x0:T0. a0A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax0 → Type[0]. + ∀a1:T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a0). + ∀T2:∀x0:T0. ∀p0:a0A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax0. ∀x1:T1 x0 p0. A href="cic:/matita/basics/logic/R1.def(2)"R1/A ?? T1 a1 ? p0 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A x1 → Type[0]. + ∀a2:T2 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a1). ∀b0:T0. - ∀e0:a0 = b0. + ∀e0:a0 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A b0. ∀b1: T1 b0 e0. - ∀e1:R1 ?? T1 a1 ? e0 = b1. + ∀e1:A href="cic:/matita/basics/logic/R1.def(2)"R1/A ?? T1 a1 ? e0 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A b1. T2 b0 e0 b1 e1. #T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1 -@(eq_rect_Type0 ????? e1) -@(R1 ?? ? ?? e0) +@(A href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/A ????? e1) +@(A href="cic:/matita/basics/logic/R1.def(2)"R1/A ?? ? ?? e0) @a2 qed. definition R3 : ∀T0:Type[0]. ∀a0:T0. - ∀T1:∀x0:T0. a0=x0 → Type[0]. - ∀a1:T1 a0 (refl ? a0). - ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0]. - ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1). - ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1. - ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0]. - ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2). + ∀T1:∀x0:T0. a0A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax0 → Type[0]. + ∀a1:T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a0). + ∀T2:∀x0:T0. ∀p0:a0A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax0. ∀x1:T1 x0 p0. A href="cic:/matita/basics/logic/R1.def(2)"R1/A ?? T1 a1 ? p0 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A x1 → Type[0]. + ∀a2:T2 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a1). + ∀T3:∀x0:T0. ∀p0:a0A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/Ax0. ∀x1:T1 x0 p0.∀p1:A href="cic:/matita/basics/logic/R1.def(2)"R1/A ?? T1 a1 ? p0 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A x1. + ∀x2:T2 x0 p0 x1 p1.A href="cic:/matita/basics/logic/R2.def(3)"R2/A ???? T2 a2 x0 p0 ? p1 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A x2 → Type[0]. + ∀a3:T3 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a1) a2 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? a2). ∀b0:T0. - ∀e0:a0 = b0. + ∀e0:a0 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A b0. ∀b1: T1 b0 e0. - ∀e1:R1 ?? T1 a1 ? e0 = b1. + ∀e1:A href="cic:/matita/basics/logic/R1.def(2)"R1/A ?? T1 a1 ? e0 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A b1. ∀b2: T2 b0 e0 b1 e1. - ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2. + ∀e2:A href="cic:/matita/basics/logic/R2.def(3)"R2/A ???? T2 a2 b0 e0 ? e1 A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A b2. T3 b0 e0 b1 e1 b2 e2. #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2 -@(eq_rect_Type0 ????? e2) -@(R2 ?? ? ???? e0 ? e1) +@(A href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/A ????? e2) +@(A href="cic:/matita/basics/logic/R2.def(3)"R2/A ?? ? ???? e0 ? e1) @a3 qed. definition R4 : ∀T0:Type[0]. ∀a0:T0. - ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0]. - ∀a1:T1 a0 (refl T0 a0). - ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0]. - ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1). - ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1. - ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0]. - ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) - a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2). - ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1. - ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2. - ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3. + ∀T1:∀x0:T0. A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A T0 a0 x0 → Type[0]. + ∀a1:T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0). + ∀T2:∀x0:T0. ∀p0:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T0 …) a0 x0. ∀x1:T1 x0 p0.A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T1 …) (A href="cic:/matita/basics/logic/R1.def(2)"R1/A T0 a0 T1 a1 x0 p0) x1 → Type[0]. + ∀a2:T2 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0)) a1). + ∀T3:∀x0:T0. ∀p0:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T1 …) (A href="cic:/matita/basics/logic/R1.def(2)"R1/A T0 a0 T1 a1 x0 p0) x1. + ∀x2:T2 x0 p0 x1 p1.A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T2 …) (A href="cic:/matita/basics/logic/R2.def(3)"R2/A T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0]. + ∀a3:T3 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0)) a1) + a2 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T2 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0)) a1)) a2). + ∀T4:∀x0:T0. ∀p0:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T1 …) (A href="cic:/matita/basics/logic/R1.def(2)"R1/A T0 a0 T1 a1 x0 p0) x1. + ∀x2:T2 x0 p0 x1 p1.∀p2:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T2 …) (A href="cic:/matita/basics/logic/R2.def(3)"R2/A T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2. + ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T3 …) (A href="cic:/matita/basics/logic/R3.def(4)"R3/A T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3. Type[0]. - ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) - a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2) - a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1) - a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)) + ∀a4:T4 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0)) a1) + a2 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T2 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0)) a1)) a2) + a3 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T3 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0)) a1) + a2 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T2 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0) a1 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A (T1 a0 (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A T0 a0)) a1)) a2)) a3). ∀b0:T0. - ∀e0:eq (T0 …) a0 b0. + ∀e0:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T0 …) a0 b0. ∀b1: T1 b0 e0. - ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1. + ∀e1:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T1 …) (A href="cic:/matita/basics/logic/R1.def(2)"R1/A T0 a0 T1 a1 b0 e0) b1. ∀b2: T2 b0 e0 b1 e1. - ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2. + ∀e2:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T2 …) (A href="cic:/matita/basics/logic/R2.def(3)"R2/A T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2. ∀b3: T3 b0 e0 b1 e1 b2 e2. - ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3. + ∀e3:A href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/A (T3 …) (A href="cic:/matita/basics/logic/R3.def(4)"R3/A T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3. T4 b0 e0 b1 e1 b2 e2 b3 e3. #T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3 -@(eq_rect_Type0 ????? e3) -@(R3 ????????? e0 ? e1 ? e2) +@(A href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/A ????? e3) +@(A href="cic:/matita/basics/logic/R3.def(4)"R3/A ????????? e0 ? e1 ? e2) @a4 qed. (* TODO concrete definition by means of proof irrelevance *) -axiom streicherK : ∀T:Type[1].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. \ No newline at end of file +axiom streicherK : ∀T:Type[1].∀t:T.∀P:t A title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/A t → Type[2].P (A href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/A ? t) → ∀p.P p. diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml index aa271b2a1..48ff2d360 100644 --- a/matitaB/matita/matitaEngine.ml +++ b/matitaB/matita/matitaEngine.ml @@ -240,7 +240,9 @@ and compile ~compiling ~asserted ~include_paths ~outch ?uid fname = (* XXX: update script -- currently to stdout *) let origbuf = Ulexing.from_utf8_channel (open_in fname) in let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in - ignore (SmallLexer.mk_small_printer interpr outch origbuf); + let outstr = ref "" in + ignore (SmallLexer.mk_small_printer interpr outstr origbuf); + Printf.fprintf outch "%s" !outstr; asserted (* MATITA 1.0: debbo fare time_travel sulla ng_library? LexiconSync.time_travel diff --git a/matitaB/matita/matitaScriptLexer.ml b/matitaB/matita/matitaScriptLexer.ml index a7ce7142f..205d14d57 100644 --- a/matitaB/matita/matitaScriptLexer.ml +++ b/matitaB/matita/matitaScriptLexer.ml @@ -342,3 +342,35 @@ let get_hot_spots = in aux 0 (aux_basic None None None) let get_hot_spots s = get_hot_spots (Ulexing.from_utf8_string s) + +(*let xmarkup = "\005" +let ymarkup = "\006" +let regexp tag_cont = ident_letter | xml_digit | "_" | "-" +let regexp tagname = ident_letter tag_cont* +let regexp opentag = xmarkup tagname +let regexp closetag = xmarkup "/" tagname ymarkup +let regexp attribute = tagname "=" qstring + +let rec to_xy = + lexer + | closetag -> xmarkup ^ ymarkup ^ xmarkup ^ to_xy lexbuf + | opentag -> + let tag = + Ulexing.utf8_sub_lexeme lexbuf 1 + (Ulexing.lexeme_length lexbuf - 1) in + xmarkup ^ ymarkup ^ tag ^ to_xy_inner lexbuf + | eof -> "" + | _ -> let lexeme = Ulexing.utf8_lexeme lexbuf in + prerr_endline ("matched " ^ lexeme); lexeme ^ to_xy lexbuf + +and to_xy_inner = + lexer + | utf8_blank+ -> to_xy_inner lexbuf + | attribute -> let lexeme = Ulexing.utf8_lexeme lexbuf in + ymarkup ^ lexeme ^ to_xy_inner lexbuf + | ">" -> xmarkup ^ to_xy lexbuf + | eof -> "" + | _ -> to_xy lexbuf +;; + +let to_xy s = to_xy (Ulexing.from_utf8_string s)*) diff --git a/matitaB/matita/matitaScriptLexer.mli b/matitaB/matita/matitaScriptLexer.mli index 29980c6db..3647fa067 100644 --- a/matitaB/matita/matitaScriptLexer.mli +++ b/matitaB/matita/matitaScriptLexer.mli @@ -31,4 +31,3 @@ exception Error of int * int * string val get_hot_spots : string -> (Stdpp.location * Stdpp.location * string option * string option) list - diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index d98a21e9b..9e6b11c6f 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -51,6 +51,17 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*) utf8_length parsed_text +(*let save_moo status = + let script = MatitaScript.current () in + let baseuri = status#baseuri in + match script#bos, script#eos with + | true, _ -> () + | _, true -> + GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) + status + | _ -> clean_current_baseuri status +;;*) + let sequent_size = ref 40;; let include_paths = ref [];; @@ -127,6 +138,23 @@ let output_status s = String.concat "\n\n" txt ;; *) +let html_of_matita s = + prerr_endline ("input: " ^ s); + let patt1 = Str.regexp "\005" in + let patt2 = Str.regexp "\006" in + let patt3 = Str.regexp "<" in + let patt4 = Str.regexp ">" in + let res = Str.global_replace patt4 ">" s in + prerr_endline ("output: " ^ res); + let res = Str.global_replace patt3 "<" res in + prerr_endline ("output: " ^ res); + let res = Str.global_replace patt2 ">" res in + prerr_endline ("output: " ^ res); + let res = Str.global_replace patt1 "<" res in + prerr_endline ("output: " ^ res); + res +;; + let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";; let first_line s = @@ -177,8 +205,10 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in prerr_endline ("reading file " ^ filename); let body = - Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () - (read_file filename) in + (* Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () + (html_of_matita (read_file filename)) in + *) + html_of_matita (read_file filename) in prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND"); let body = "" ^ body ^ "" in let baseuri, incpaths = @@ -212,14 +242,24 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let advance0 sid text = let status = MatitaAuthentication.get_status sid in let history = MatitaAuthentication.get_history sid in + let status = status#reset_disambiguate_db () in let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len = - (* try *) + try eval_statement !include_paths (*buffer*) status (`Raw text) - (* with End_of_file -> raise Margin *) + with + | HExtlib.Localized (_,e) -> raise e + (*| End_of_file -> raise Margin *) in + let stringbuf = Ulexing.from_utf8_string new_statements in + let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in + let outstr = ref "" in + ignore (SmallLexer.mk_small_printer interpr outstr stringbuf); + prerr_endline ("parser output: " ^ !outstr); MatitaAuthentication.set_status sid st; MatitaAuthentication.set_history sid (st::history); - parsed_len, new_unparsed, st + parsed_len, + Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false + () (html_of_matita !outstr), new_unparsed, st let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in @@ -321,10 +361,11 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (); let text = cgi#argument_value "body" in prerr_endline ("body =\n" ^ text); - let parsed_len, new_unparsed, new_status = advance0 sid text in + let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in let txt = output_status new_status in let body = - "" ^ txt + "" ^ + new_parsed ^ "" ^ txt ^ "" in prerr_endline ("sending advance response:\n" ^ body); @@ -346,13 +387,18 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in - let rec aux parsed_len text = + let rec aux parsed_len parsed_txt text = try prerr_endline ("evaluating: " ^ first_line text); - let plen,new_unparsed,_new_status = advance0 sid text in - aux (parsed_len+plen) new_unparsed + let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in + aux (parsed_len+plen) (parsed_txt ^ new_parsed) new_unparsed with - | _ -> parsed_len + | End_of_file -> + let status = MatitaAuthentication.get_status sid in + GrafiteTypes.Serializer.serialize + ~baseuri:(NUri.uri_of_string status#baseuri) status; + parsed_len, parsed_txt + | _ -> parsed_len, parsed_txt in cgi # set_header ~cache:`No_cache @@ -360,13 +406,18 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (); let text = cgi#argument_value "body" in prerr_endline ("body =\n" ^ text); - let parsed_len = aux 0 text in + let parsed_len, new_parsed = aux 0 "" text in let status = MatitaAuthentication.get_status sid in let txt = output_status status in let body = - "" ^ txt + "" ^ + new_parsed ^ "" ^ txt ^ "" in + (*let body = + "" ^ txt + ^ "" + in*) prerr_endline ("sending goto bottom response:\n" ^ body); cgi#out_channel#output_string body with Not_found -> cgi#set_header ~status:`Internal_server_error diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index e4b0efdba..04787ce77 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -349,15 +349,33 @@ String.prototype.sescape = function() { return (result); } -String.prototype.unescapeHTML = function() +String.prototype.html_to_matita = function() { var patt1 = //gi; - var patt2 = /</gi; - var patt3 = />/gi; + var patt2 = //gi + var patt4 = /</gi; + var patt5 = />/gi; var result = this; result = result.replace(patt1,"\n"); - result = result.replace(patt2,"<"); - result = result.replace(patt3,">"); + result = result.replace(patt2,"\005"); + result = result.replace(patt3,"\006"); + result = result.replace(patt4,"<"); + result = result.replace(patt5,">"); + return (unescape(result)); +} + +String.prototype.matita_to_html = function() +{ + var patt1 = //gi + var patt3 = /\005/gi; + var patt4 = /\006/gi; + var result = this; + result = result.replace(patt1,"<"); + result = result.replace(patt2,">"); + result = result.replace(patt3,"<"); + result = result.replace(patt4,">"); return (unescape(result)); } @@ -449,13 +467,15 @@ function advanceForm1() processor = function(xml) { if (is_defined(xml)) { // debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND"); - len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length")); + parsed = xml.getElementsByTagName("parsed")[0]; + len = parseInt(parsed.getAttribute("length")); len0 = unlocked.innerHTML.length; - unescaped = unlocked.innerHTML.unescapeHTML(); - parsedtxt = unescaped.substr(0,len); + unescaped = unlocked.innerHTML.html_to_matita(); + parsedtxt = parsed.childNodes[0].nodeValue; + //parsedtxt = unescaped.substr(0,len); unparsedtxt = unescaped.substr(len); - locked.innerHTML = locked.innerHTML + parsedtxt; - unlocked.innerHTML = unparsedtxt; + locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html(); + unlocked.innerHTML = unparsedtxt.matita_to_html(); len1 = unlocked.innerHTML.length; len2 = len0 - len1; metasenv = xml.getElementsByTagName("meta"); @@ -468,7 +488,7 @@ function advanceForm1() resume(); }; pause(); - callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape()); + callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); } @@ -477,13 +497,15 @@ function gotoBottom() processor = function(xml) { if (is_defined(xml)) { // debug("goto bottom: received response\nBEGIN\n" + req.responseText + "\nEND"); - len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length")); + parsed = xml.getElementsByTagName("parsed")[0]; + len = parseInt(parsed.getAttribute("length")); len0 = unlocked.innerHTML.length; - unescaped = unlocked.innerHTML.unescapeHTML(); - parsedtxt = unescaped.substr(0,len); + unescaped = unlocked.innerHTML.html_to_matita(); + parsedtxt = parsed.childNodes[0].nodeValue; + //parsedtxt = unescaped.substr(0,len); unparsedtxt = unescaped.substr(len); - locked.innerHTML = locked.innerHTML + parsedtxt; - unlocked.innerHTML = unparsedtxt; + locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html(); + unlocked.innerHTML = unparsedtxt.matita_to_html(); len1 = unlocked.innerHTML.length; len2 = len0 - len1; metasenv = xml.getElementsByTagName("meta"); @@ -496,7 +518,7 @@ function gotoBottom() resume(); }; pause(); - callServer("bottom",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape()); + callServer("bottom",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); } @@ -508,14 +530,15 @@ function gotoPos(offset) } processor = function(xml) { if (is_defined(xml)) { - // debug("goto pos: received response\nBEGIN\n" + req.responseText + "\nEND"); - len = parseInt(xml.getElementsByTagName("parsed")[0].getAttribute("length")); + parsed = xml.getElementsByTagName("parsed")[0]; + len = parseInt(parsed.getAttribute("length")); len0 = unlocked.innerHTML.length; - unescaped = unlocked.innerHTML.unescapeHTML(); - parsedtxt = unescaped.substr(0,len); + unescaped = unlocked.innerHTML.html_to_matita(); + parsedtxt = parsed.childNodes[0].nodeValue; + //parsedtxt = unescaped.substr(0,len); unparsedtxt = unescaped.substr(len); - locked.innerHTML = locked.innerHTML + parsedtxt; - unlocked.innerHTML = unparsedtxt; + locked.innerHTML = locked.innerHTML + parsedtxt; //.matita_to_html(); + unlocked.innerHTML = unparsedtxt.matita_to_html(); len1 = unlocked.innerHTML.length; len2 = len0 - len1; metasenv = xml.getElementsByTagName("meta"); @@ -536,7 +559,7 @@ function gotoPos(offset) } } pause(); - callServer("advance",processor,"body=" + (unlocked.innerHTML.unescapeHTML()).sescape()); + callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape()); } function retract() @@ -584,6 +607,7 @@ function retrieveFile(thefile) { if (is_defined(xml)) { locked.innerHTML = ""; + debug(xml.documentElement.textContent); unlocked.innerHTML = xml.documentElement.textContent; } else { debug("file open failed");