summaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/metasyntax.ml24
-rw-r--r--toplevel/mltop.ml44
-rw-r--r--toplevel/toplevel.ml13
-rw-r--r--toplevel/vernacentries.ml10
4 files changed, 25 insertions, 26 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6a75b99c..821a73f7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: metasyntax.ml 11786 2009-01-14 13:07:34Z herbelin $ *)
+(* $Id: metasyntax.ml 12882 2010-03-23 22:34:38Z herbelin $ *)
open Pp
open Util
@@ -266,16 +266,18 @@ let split_notation_string str =
(* Interpret notations with a recursive component *)
-let rec find_pattern xl = function
- | Break n as x :: l, Break n' :: l' when n=n' ->
- find_pattern (x::xl) (l,l')
+let out_nt = function NonTerminal x -> x | _ -> assert false
+
+let rec find_pattern nt xl = function
+ | Break n as x :: l, Break n' :: l' when n=n' ->
+ find_pattern nt (x::xl) (l,l')
| Terminal s as x :: l, Terminal s' :: l' when s = s' ->
- find_pattern (x::xl) (l,l')
- | [NonTerminal x], NonTerminal x' :: l' ->
- (x,x',xl),l'
- | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ ->
+ find_pattern nt (x::xl) (l,l')
+ | [], NonTerminal x' :: l' ->
+ (out_nt nt,x',List.rev xl),l'
+ | [], Terminal s :: _ | Terminal s :: _, _ ->
error ("The token "^s^" occurs on one side of \"..\" but not on the other side.")
- | [NonTerminal _], Break s :: _ | Break s :: _, _ ->
+ | [], Break s :: _ | Break s :: _, _ ->
error ("A break occurs on one side of \"..\" but not on the other side.")
| ((SProdList _ | NonTerminal _) :: _ | []), _ ->
error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\".")
@@ -283,7 +285,8 @@ let rec find_pattern xl = function
let rec interp_list_parser hd = function
| [] -> [], [], List.rev hd
| NonTerminal id :: tl when id = ldots_var ->
- let ((x,y,sl),tl') = find_pattern [] (hd,tl) in
+ let hd = List.rev hd in
+ let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
let yl,xl,tl'' = interp_list_parser [] tl' in
(* We remember each pair of variable denoting a recursive part to *)
(* remove the second copy of it afterwards *)
@@ -299,6 +302,7 @@ let rec interp_list_parser hd = function
yl, xl, List.rev_append hd tl'
| SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
+
(* Find non-terminal tokens of notation *)
let unquote_notation_token s =
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 176f336b..b54700d3 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -11,7 +11,7 @@
* camlp4deps will not work for this file unless Makefile system enhanced.
*)
-(* $Id: mltop.ml4 11801 2009-01-18 20:11:41Z herbelin $ *)
+(* $Id: mltop.ml4 12341 2009-09-17 16:03:19Z glondu $ *)
open Util
open Pp
@@ -109,7 +109,7 @@ let dir_ml_load s =
* in this file, the Makefile dependency logic needs to be updated.
*)
let warn = Flags.is_verbose() in
- let _,gname = where_in_path ~warn !coq_mlpath_copy s in
+ let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in
try
Dynlink.loadfile gname;
with | Dynlink.Error a ->
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index a1acd1d6..9d64f983 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: toplevel.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: toplevel.ml 12891 2010-03-30 11:40:02Z herbelin $ *)
open Pp
open Util
@@ -163,11 +163,10 @@ let print_location_in_file s inlibrary fname loc =
try
let (line, bol) = line_of_pos 1 0 0 in
close_in ic;
- hov 0
- (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++ str"," ++ spc() ++
- hov 0 (str"line " ++ int line ++ str"," ++ spc() ++
- str"characters " ++
- Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":") ++
+ hov 0 (* No line break so as to follow emacs error message format *)
+ (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++
+ str", line " ++ int line ++ str", characters " ++
+ Cerrors.print_loc (make_loc (bp-bol,ep-bol))) ++ str":" ++
fnl ()
with e ->
(close_in ic;
@@ -316,7 +315,7 @@ let parse_to_dot =
let rec discard_to_dot () =
try
Gram.Entry.parse parse_to_dot top_buffer.tokens
- with Stdpp.Exc_located(_,Token.Error _) ->
+ with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) ->
discard_to_dot()
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 6a0acb52..385afbec 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: vernacentries.ml 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id: vernacentries.ml 12343 2009-09-17 17:02:03Z glondu $ i*)
(* Concrete syntax of the mathematical vernacular MV V2.6 *)
@@ -234,12 +234,8 @@ let dump_universes s =
(* "Locate" commands *)
let locate_file f =
- try
- let _,file = System.where_in_path ~warn:false (Library.get_load_paths ()) f in
- msgnl (str file)
- with Not_found ->
- msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
- str"on loadpath"))
+ let _,file = System.find_file_in_path ~warn:false (Library.get_load_paths ()) f in
+ msgnl (str file)
let msg_found_library = function
| Library.LibLoaded, fulldir, file ->