diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-05 11:46:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-05 11:46:28 +0000 |
| commit | 20720975c49e5c48f6b03a96df0186b56557eb3e (patch) | |
| tree | 79cfbebb13fadb558e87f903eed42363fc98671d /lib | |
| parent | b37ceca4e2c6e39050ade2acef314dfed24c8e49 (diff) | |
Correction de quelques défauts d'affichage (notations sous "as" pour
filtrage; sauts de line intempestifs dans pretty.ml)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10179 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/pp.ml4 | 2 | ||||
| -rw-r--r-- | lib/pp.mli | 1 |
2 files changed, 3 insertions, 0 deletions
diff --git a/lib/pp.ml4 b/lib/pp.ml4 index bfabb533b..415a3002a 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -140,6 +140,8 @@ let strbrk s = else if p=n then [< >] else [< str (String.sub s p (n-p)) >] in aux 0 0 +let ismt s = try let _ = Stream.empty s in true with Stream.Failure -> false + (* boxing commands *) let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >] let v n s = [< 'Ppcmd_box(Pp_vbox n,s) >] diff --git a/lib/pp.mli b/lib/pp.mli index 8a5aee799..41ea9ca0f 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -35,6 +35,7 @@ val fnl : unit -> std_ppcmds val pifb : unit -> std_ppcmds val ws : int -> std_ppcmds val mt : unit -> std_ppcmds +val ismt : std_ppcmds -> bool val comment : int -> std_ppcmds val comments : ((int * int) * string) list ref |