← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to interp/notation.ml

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
interp/notation.ml
1
1
(************************************************************************)
2
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
3
 
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 
3
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
4
4
(*   \VV/  **************************************************************)
5
5
(*    //   *      This file is distributed under the terms of the       *)
6
6
(*         *       GNU Lesser General Public License Version 2.1        *)
7
7
(************************************************************************)
8
8
 
9
 
(* $Id: notation.ml 13463 2010-09-24 22:21:29Z herbelin $ *)
 
9
(* $Id: notation.ml 14820 2011-12-18 22:11:32Z herbelin $ *)
10
10
 
11
11
(*i*)
12
12
open Util
328
328
  let (key,n) = aconstr_key c in
329
329
  notations_key_table := Gmapl.add key (rule,pat,n) !notations_key_table
330
330
 
331
 
let rec find_interpretation find = function
 
331
let rec find_interpretation ntn find = function
332
332
  | [] -> raise Not_found
333
 
  | sce :: scopes ->
334
 
      let sc,sco = match sce with
335
 
        | Scope sc -> sc, Some sc
336
 
        | SingleNotation _ -> default_scope, None in
337
 
      try
338
 
        let (pat,df) = find sc in
339
 
        pat,(df,sco)
340
 
      with Not_found ->
341
 
        find_interpretation find scopes
 
333
  | Scope scope :: scopes ->
 
334
      (try let (pat,df) = find scope in pat,(df,Some scope)
 
335
       with Not_found -> find_interpretation ntn find scopes)
 
336
  | SingleNotation ntn'::scopes when ntn' = ntn ->
 
337
      (try let (pat,df) = find default_scope in pat,(df,None)
 
338
       with Not_found ->
 
339
         (* e.g. because single notation only for constr, not cases_pattern *)
 
340
         find_interpretation ntn find scopes)
 
341
  | SingleNotation _::scopes ->
 
342
      find_interpretation ntn find scopes
342
343
 
343
344
let find_notation ntn sc =
344
345
  Gmap.find ntn (find_scope sc).notations
361
362
 
362
363
let interp_prim_token_gen g loc p local_scopes =
363
364
  let scopes = make_current_scopes local_scopes in
364
 
  try find_interpretation (find_prim_token g loc p) scopes
 
365
  let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in
 
366
  try find_interpretation p_as_ntn (find_prim_token g loc p) scopes
365
367
  with Not_found ->
366
368
    user_err_loc (loc,"interp_prim_token",
367
369
    (match p with
376
378
 
377
379
let rec interp_notation loc ntn local_scopes =
378
380
  let scopes = make_current_scopes local_scopes in
379
 
  try find_interpretation (find_notation ntn) scopes
 
381
  try find_interpretation ntn (find_notation ntn) scopes
380
382
  with Not_found ->
381
383
    user_err_loc
382
384
    (loc,"",str ("Unknown interpretation for notation \""^ntn^"\"."))