diff options
| author | herbelin | 2002-12-21 10:33:15 +0000 |
|---|---|---|
| committer | herbelin | 2002-12-21 10:33:15 +0000 |
| commit | edfc0dd4667f6d925f6492f593d51cd157cae620 (patch) | |
| tree | c37fd72ad95ae2e6b1cda1ff72bdd227276a8d00 /toplevel | |
| parent | c538feb03d46be62f04af35cc90baf2124afcbc1 (diff) | |
Affinement affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3471 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 76005c00e5..ffa233ba22 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -226,6 +226,7 @@ let precedence_of_entry_type = function | ETConstr (n,BorderProd (left,Some a)) -> n, let (lp,rp) = prec_assoc a in if left then lp else rp | ETConstr (n,InternalProd) -> n, Prec n + | ETOther ("constr","annot") -> 10, Prec 10 | _ -> 0, E (* ?? *) (* x = y |-> x brk = y (breaks before any symbol) *) @@ -271,6 +272,10 @@ let is_bracket s = (s.[0] = '{' or s.[0] = '[' or s.[0] = '(' or s.[l-1] = '}' or s.[l-1] = ']' or s.[l-1] = ')') +let is_comma s = + let l = String.length s in l <> 0 & + (s.[0] = ',' or s.[0] = ';' or s.[0] = ':') + let is_operator s = let l = String.length s in l <> 0 & (s.[0] = '+' or s.[0] = '*' or s.[0] = '=' or @@ -292,18 +297,19 @@ let make_hunks etyps symbols = let nextsep,(s,l) = if is_letter (s.[0]) or - is_letter (s.[String.length s -1]) or - is_digit (s.[String.length s -1]) + (ws = NextIsTerminal & + (is_letter (s.[String.length s -1])) or + (is_digit (s.[String.length s -1]))) then (* We want spaces around both sides *) Separate 1, if ws = Separate 0 then s^" ",l else s,add_break l ws else - (* We want a break before symbols but brackets*) - if is_bracket s then + (* We want a break before symbols but brackets and commas *) + if is_bracket s or is_comma s then Juxtapose, (s,if ws = Separate 0 then add_break l ws else l) - else + else Separate 0, (s,l) in (nextsep, UnpTerminal s :: l) |