From f9512e878bd27f8cb5261bb18b0da0d42c8184d0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 25 Oct 2006 12:41:21 +0000 Subject: [PATCH] 1. bug fixed: Unicode characters that are not mapped to TeX macros used to be post-fixed with a blank 2. bug fixed: the textual pretty-printer does not implement the same spacing politics of GtkMathView. Since that politics is very very complex to implement, I try a different solution: we explicitly insert a space where we want one. The widget does not seem to be disturbed by this. This way the let ... rec and match ... with constructs are now printed correctly and they can be read back. 3. syntax change: applicative patterns no longer require parentheses around them --- components/content_pres/boxPp.ml | 13 +++++++------ components/content_pres/cicNotationParser.ml | 1 + components/content_pres/cicNotationPres.ml | 2 +- components/content_pres/termContentPres.ml | 13 +++++++++---- components/grafite_parser/print_grammar.ml | 4 ++++ components/syntax_extensions/utf8Macro.ml | 7 +++++-- components/syntax_extensions/utf8Macro.mli | 3 +-- matita/help/C/sec_terms.xml | 6 ++++++ 8 files changed, 34 insertions(+), 15 deletions(-) diff --git a/components/content_pres/boxPp.ml b/components/content_pres/boxPp.ml index 53149877e..b9bb9fbbd 100644 --- a/components/content_pres/boxPp.ml +++ b/components/content_pres/boxPp.ml @@ -193,13 +193,14 @@ let render_to_strings choose_action size markup = | Pres.Mgliph (_, s) -> fixed_rendering s | Pres.Mo (_, s) -> let s = - if String.length s > 1 then - (* heuristic to guess which operators need to be expanded in their - * TeX like format *) - Utf8Macro.tex_of_unicode s ^ " " - else s + if String.length s = 1 && Char.code s.[0] < 128 then + s + else + match Utf8Macro.tex_of_unicode s with + Some s -> s ^ " " + | None -> s in - fixed_rendering s + fixed_rendering s | Pres.Mspace _ -> fixed_rendering string_space | Pres.Mrow (attrs, children) -> let children' = List.map aux_mpres children in diff --git a/components/content_pres/cicNotationParser.ml b/components/content_pres/cicNotationParser.ml index 088d1b69d..69ae68aee 100644 --- a/components/content_pres/cicNotationParser.ml +++ b/components/content_pres/cicNotationParser.ml @@ -458,6 +458,7 @@ EXTEND [ id = IDENT -> id, None, [] | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN -> id, None, vars + | id = IDENT; vars = LIST1 possibly_typed_name -> id, None, vars ] ]; binder: [ diff --git a/components/content_pres/cicNotationPres.ml b/components/content_pres/cicNotationPres.ml index 4198e83b0..673df335f 100644 --- a/components/content_pres/cicNotationPres.ml +++ b/components/content_pres/cicNotationPres.ml @@ -357,7 +357,7 @@ let render ids_to_uris ?(prec=(-1)) = let attrs = make_href xmlattrs xref in (match l with | `Symbol s -> Mpres.Mo (attrs, to_unicode s) - | `Keyword s -> Mpres.Mo (attrs, to_unicode s) + | `Keyword s -> Mpres.Mtext (attrs, to_unicode s) | `Number s -> Mpres.Mn (attrs, to_unicode s)) and aux_layout mathonly xref pos prec l = let attrs = make_xref xref in diff --git a/components/content_pres/termContentPres.ml b/components/content_pres/termContentPres.ml index e925db0aa..a8bfe1147 100644 --- a/components/content_pres/termContentPres.ml +++ b/components/content_pres/termContentPres.ml @@ -75,6 +75,7 @@ let vbox = box Ast.V let hvbox = box Ast.HV let hovbox = box Ast.HOV let break = Ast.Layout Ast.Break +let space = Ast.Literal (`Symbol " ") let builtin_symbol s = Ast.Literal (`Symbol s) let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k)) @@ -128,24 +129,26 @@ let pp_ast0 t k = match outty_opt with | None -> [] | Some outty -> - [ keyword "return"; break; remove_level_info (k outty)] + [ space; keyword "return"; space; break; remove_level_info (k outty)] in let indty_box = match indty_opt with | None -> [] - | Some (indty, href) -> [ keyword "in"; break; ident_w_href href indty ] + | Some (indty, href) -> [ space; keyword "in"; space; break; ident_w_href href indty ] in let match_box = hvbox false false [ hvbox false true [ - hvbox false true [ keyword "match"; break; top_pos (k what) ]; + hvbox false true [keyword "match"; space; break; top_pos (k what)]; break; hvbox false true indty_box; break; hvbox false true outty_box ]; break; - keyword "with" + space; + keyword "with"; + space ] in let mk_case_pattern (head, href, vars) = @@ -216,7 +219,9 @@ let pp_ast0 t k = let (params, name, ty, body) = fst_fun in hvbox false true ([ keyword "let"; + space; keyword rec_op; + space; name] @ params @ (match ty with None -> [] | Some ty -> [builtin_symbol ":"; ty]) @ diff --git a/components/grafite_parser/print_grammar.ml b/components/grafite_parser/print_grammar.ml index 6a05865de..f05b77a11 100644 --- a/components/grafite_parser/print_grammar.ml +++ b/components/grafite_parser/print_grammar.ml @@ -28,11 +28,15 @@ open Gramext let tex_of_unicode s = +(*CSC: ??????? What's the meaning of this function? let contractions = ("\\Longrightarrow","=>") :: [] in if String.length s <= 1 then s else (* probably an extended unicode symbol *) let s = Utf8Macro.tex_of_unicode s in try List.assoc s contractions with Not_found -> s +*) match Utf8Macro.tex_of_unicode s with + Some s -> s + | None -> s let needs_brackets t = let rec count_brothers = function diff --git a/components/syntax_extensions/utf8Macro.ml b/components/syntax_extensions/utf8Macro.ml index e5fca10c4..36d6b175d 100644 --- a/components/syntax_extensions/utf8Macro.ml +++ b/components/syntax_extensions/utf8Macro.ml @@ -41,7 +41,10 @@ let unicode_of_tex s = with Macro_not_found _ -> s let tex_of_unicode s = + (*WARNING: the space below is a nbsp (0x00A0), not a normal space *) + if s = " " then Some "" + else try - "\\" ^ Hashtbl.find Utf8MacroTable.utf82macro s - with Not_found -> s + Some ("\\" ^ Hashtbl.find Utf8MacroTable.utf82macro s) + with Not_found -> None diff --git a/components/syntax_extensions/utf8Macro.mli b/components/syntax_extensions/utf8Macro.mli index d92f60b37..b21ba504f 100644 --- a/components/syntax_extensions/utf8Macro.mli +++ b/components/syntax_extensions/utf8Macro.mli @@ -36,5 +36,4 @@ val expand: string -> string val unicode_of_tex: string -> string (** ... the other way round *) -val tex_of_unicode: string -> string - +val tex_of_unicode: string -> string option diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml index 65000b9ba..5f682eb83 100644 --- a/matita/help/C/sec_terms.xml +++ b/matita/help/C/sec_terms.xml @@ -387,6 +387,12 @@ (&id; &id; [&id;]…) n-ary constructor (binds the n arguments) + + + | + &id; &id; [&id;]… + n-ary constructor (binds the n arguments) + -- 2.39.2