From a77f70a077dfffd6b9b161799bd6f19c9dcf3706 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Tue, 6 Nov 2012 18:50:10 +0100
Subject: [PATCH] Add support for operators to why3doc.

---
 src/parser/parser.mly     |  3 ++-
 src/why3doc/doc_lexer.mll | 23 ++++++++++++++++++++++-
 2 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/src/parser/parser.mly b/src/parser/parser.mly
index ff55fc6c0..552c4a60a 100644
--- a/src/parser/parser.mly
+++ b/src/parser/parser.mly
@@ -886,8 +886,9 @@ ident_rich:
 
 lident_rich:
 | lident                      { $1 }
-| LEFTPAR lident_op RIGHTPAR  { mk_id $2 (floc ()) }
+| LEFTPAR lident_op RIGHTPAR  { mk_id $2 (floc_i 2) }
 | LEFTPAR_STAR_RIGHTPAR       { mk_id (infix "*") (floc ()) }
+  /* FIXME: use location of operator star rather than left parenthesis */
 ;
 
 lident_op:
diff --git a/src/why3doc/doc_lexer.mll b/src/why3doc/doc_lexer.mll
index 4e008e166..bb92b602e 100644
--- a/src/why3doc/doc_lexer.mll
+++ b/src/why3doc/doc_lexer.mll
@@ -83,8 +83,29 @@
 
 }
 
+let op_char_1 = ['=' '<' '>' '~']
+let op_char_2 = ['+' '-']
+let op_char_3 = ['*' '/' '%']
+let op_char_4 = ['!' '$' '&' '?' '@' '^' '.' ':' '|' '#']
+let op_char_34 = op_char_3 | op_char_4
+let op_char_234 = op_char_2 | op_char_34
+let op_char_1234 = op_char_1 | op_char_234
+let op_char_pref = ['!' '?']
+let prefix_op =
+    op_char_1234* op_char_1 op_char_1234*
+  | op_char_234*  op_char_2 op_char_234*
+  | op_char_34* op_char_3 op_char_34*
+  | op_char_4+
+let operator =
+    op_char_pref op_char_4*
+  | prefix_op
+  | prefix_op '_'
+  | "[]"
+  | "[<-]"
+  | "[]<-"
+
 let space = [' ' '\t']
-let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']*
+let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* | operator
 let special = ['<' '>' '&']
 
 rule scan fmt = parse
-- 
GitLab