diff options
author | Stephane Glondu <steph@glondu.net> | 2010-12-24 12:51:11 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-12-24 12:51:11 +0100 |
commit | 20d03a28285c430740d0b675583fe5c4d13ffecc (patch) | |
tree | 36bd87c5c42d948291605fc35b4b7cf573fc8113 /tools/coqdoc/cpretty.mll | |
parent | c0a92523eaa76afabcbaf06ac4a7e8f7930ee4a3 (diff) | |
parent | 50dc9067e98ca001ad2e875011abab5da6fdb621 (diff) |
Merge commit 'upstream/8.3.pl1+dfsg' into experimental/master
Diffstat (limited to 'tools/coqdoc/cpretty.mll')
-rw-r--r-- | tools/coqdoc/cpretty.mll | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index a23a4f74..177058b3 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cpretty.mll 13440 2010-09-19 20:21:12Z herbelin $ i*) +(*i $Id: cpretty.mll 13692 2010-12-06 23:55:10Z herbelin $ i*) (*s Utility functions for the scanners *) @@ -272,7 +272,9 @@ let firstchar = (* superscript 1 *) '\194' '\185' | (* utf-8 latin 1 supplement *) - '\195' ['\128'-'\191'] | + '\195' ['\128'-'\150'] | + '\195' ['\152'-'\182'] | + '\195' ['\184'-'\191'] | (* utf-8 letterlike symbols *) (* '\206' ([ '\145' - '\183'] | '\187') | *) (* '\xCF' [ '\x00' - '\xCE' ] | *) @@ -315,7 +317,6 @@ let def_token = | "Class" | "SubClass" | "Example" - | "Local" | "Fixpoint" | "Boxed" | "CoFixpoint" @@ -450,6 +451,12 @@ rule coq_bol = parse { begin_show (); coq_bol lexbuf } | space* end_show { end_show (); coq_bol lexbuf } + | space* ("Local"|"Global") + { + in_proof := None; + let s = lexeme lexbuf in + output_indented_keyword s lexbuf; + coq_bol lexbuf } | space* gallina_kw_to_hide { let s = lexeme lexbuf in if !Cdglobals.light && section_or_end s then |