loc.mli 2.24 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
5 6 7 8 9
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(********************************************************************)
10 11 12

open Format

13
(* Lexing locations *)
14

15 16 17
val current_offset : int ref
val reloc : Lexing.position -> Lexing.position
val set_file : string -> Lexing.lexbuf -> unit
18

19 20
val transfer_loc : Lexing.lexbuf -> Lexing.lexbuf -> unit

21
(* locations in files *)
22

23
type position
24

25 26
val extract : Lexing.position * Lexing.position -> position
val join : position -> position -> position
27 28 29

val dummy_position : position

30
val user_position : string -> int -> int -> int -> position
31

32
val get : position -> string * int * int * int
33

34
val compare : position -> position -> int
35 36
val equal : position -> position -> bool
val hash : position -> int
37 38 39

val gen_report_position : formatter -> position -> unit

40
val report_position : formatter -> position -> unit
41

42 43 44 45
(* located exceptions *)

exception Located of position * exn

46 47 48
val try1: ?loc:position -> ('a -> 'b) -> ('a -> 'b)
val try2: ?loc:position -> ('a -> 'b -> 'c) -> ('a -> 'b -> 'c)
val try3: ?loc:position -> ('a -> 'b -> 'c -> 'd) -> ('a -> 'b -> 'c -> 'd)
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
49

50
val try4: ?loc:position ->
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
51 52
  ('a -> 'b -> 'c -> 'd -> 'e) -> ('a -> 'b -> 'c -> 'd -> 'e)

53
val try5: ?loc:position ->
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
54 55
  ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> ('a -> 'b -> 'c -> 'd -> 'e -> 'f)

56
val try6: ?loc:position ->
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
57 58 59
  ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) ->
  ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g)

60
val try7: ?loc:position ->
Andrei Paskevich's avatar
minor  
Andrei Paskevich committed
61 62
  ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) ->
  ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h)
63 64 65 66 67 68 69 70

val error: ?loc:position -> exn -> 'a

(* messages *)

exception Message of string

val errorm: ?loc:position -> ('a, Format.formatter, unit, 'b) format4 -> 'a
71 72

val with_location: (Lexing.lexbuf -> 'a) -> (Lexing.lexbuf -> 'a)