From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 8 Jul 2014 13:46:10 +0000 (+0000)
Subject: update for CamlP5
X-Git-Tag: make_still_working~876
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bc5516f15988620e9b152c6c741daae4a4c4fb0c;p=helm.git
update for CamlP5
---
diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt
index f17459162..4ee9ad4e6 100644
--- a/helm/software/components/binaries/transcript/.depend.opt
+++ b/helm/software/components/binaries/transcript/.depend.opt
@@ -1,24 +1,24 @@
-gallina8Parser.cmi: types.cmx
-grafiteParser.cmi: types.cmx
-grafite.cmi: types.cmx
-engine.cmi:
-types.cmo:
-types.cmx:
-options.cmo:
-options.cmx:
-gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi
-gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
-gallina8Lexer.cmo: options.cmx gallina8Parser.cmi
-gallina8Lexer.cmx: options.cmx gallina8Parser.cmx
-grafiteParser.cmo: types.cmx options.cmx grafiteParser.cmi
-grafiteParser.cmx: types.cmx options.cmx grafiteParser.cmi
-grafiteLexer.cmo: options.cmx grafiteParser.cmi
-grafiteLexer.cmx: options.cmx grafiteParser.cmx
-grafite.cmo: types.cmx options.cmx grafite.cmi
-grafite.cmx: types.cmx options.cmx grafite.cmi
+gallina8Parser.cmi: types.cmx
+grafiteParser.cmi: types.cmx
+grafite.cmi: types.cmx
+engine.cmi:
+types.cmo:
+types.cmx:
+options.cmo:
+options.cmx:
+gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi
+gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
+gallina8Lexer.cmo: options.cmx gallina8Parser.cmi
+gallina8Lexer.cmx: options.cmx gallina8Parser.cmx
+grafiteParser.cmo: types.cmx options.cmx grafiteParser.cmi
+grafiteParser.cmx: types.cmx options.cmx grafiteParser.cmi
+grafiteLexer.cmo: options.cmx grafiteParser.cmi
+grafiteLexer.cmx: options.cmx grafiteParser.cmx
+grafite.cmo: types.cmx options.cmx grafite.cmi
+grafite.cmx: types.cmx options.cmx grafite.cmi
engine.cmo: types.cmx options.cmx grafiteParser.cmi grafiteLexer.cmx \
- grafite.cmi gallina8Parser.cmi gallina8Lexer.cmx engine.cmi
+ grafite.cmi gallina8Parser.cmi gallina8Lexer.cmx engine.cmi
engine.cmx: types.cmx options.cmx grafiteParser.cmx grafiteLexer.cmx \
- grafite.cmx gallina8Parser.cmx gallina8Lexer.cmx engine.cmi
-top.cmo: options.cmx engine.cmi
-top.cmx: options.cmx engine.cmx
+ grafite.cmx gallina8Parser.cmx gallina8Lexer.cmx engine.cmi
+top.cmo: options.cmx engine.cmi
+top.cmx: options.cmx engine.cmx
diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 95b688c54..587c22e4a 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -211,8 +211,8 @@ let extract_term_production pattern =
match magic with
| Ast.List0 (_, None) -> Gramext.Slist0 s
| Ast.List1 (_, None) -> Gramext.Slist1 s
- | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
- | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
+ | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l, false)
+ | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l, false)
| _ -> assert false
in
[ Env (List.map Env.list_declaration p_names),
@@ -819,11 +819,11 @@ let exc_located_wrapper f =
try
f ()
with
- | Stdpp.Exc_located (floc, Stream.Error msg) ->
+ | Ploc.Exc (floc, Stream.Error msg) ->
raise (HExtlib.Localized (floc, Parse_error msg))
- | Stdpp.Exc_located (floc, HExtlib.Localized (_,exn)) ->
+ | Ploc.Exc (floc, HExtlib.Localized (_,exn)) ->
raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
- | Stdpp.Exc_located (floc, exn) ->
+ | Ploc.Exc (floc, exn) ->
raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
let parse_level1_pattern precedence lexbuf =
diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 941bb2218..b1362b0f6 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -1058,13 +1058,13 @@ let exc_located_wrapper f =
try
f ()
with
- | Stdpp.Exc_located (_, End_of_file) -> raise End_of_file
- | Stdpp.Exc_located (floc, Stream.Error msg) ->
+ | Ploc.Exc (_, End_of_file) -> raise End_of_file
+ | Ploc.Exc (floc, Stream.Error msg) ->
raise (HExtlib.Localized (floc,CicNotationParser.Parse_error msg))
- | Stdpp.Exc_located (floc, HExtlib.Localized(_,exn)) ->
+ | Ploc.Exc (floc, HExtlib.Localized(_,exn)) ->
raise
(HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
- | Stdpp.Exc_located (floc, exn) ->
+ | Ploc.Exc (floc, exn) ->
raise
(HExtlib.Localized (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
diff --git a/helm/software/components/grafite_parser/print_grammar.ml b/helm/software/components/grafite_parser/print_grammar.ml
index 893a3f53c..47f42356f 100644
--- a/helm/software/components/grafite_parser/print_grammar.ml
+++ b/helm/software/components/grafite_parser/print_grammar.ml
@@ -87,7 +87,7 @@ and is_symbol_dummy = function
| Smeta (_, lt, _) -> List.for_all is_symbol_dummy lt
| Snterm e | Snterml (e, _) -> is_entry_dummy e
| Slist1 x | Slist0 x -> is_symbol_dummy x
- | Slist1sep (x,y) | Slist0sep (x,y) -> is_symbol_dummy x && is_symbol_dummy y
+ | Slist1sep (x,y,false) | Slist0sep (x,y,false) -> is_symbol_dummy x && is_symbol_dummy y
| Sopt x -> is_symbol_dummy x
| Sself | Snext -> false
| Stree t -> is_tree_dummy t
@@ -186,7 +186,7 @@ let visit_description desc fmt self =
let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "@]} @ ";
todo
- | Slist0sep (symbol,sep) ->
+ | Slist0sep (symbol,sep,false) ->
Format.fprintf fmt "[@[<hov2> ";
let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "{@[<hov2> ";
@@ -200,7 +200,7 @@ let visit_description desc fmt self =
let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "@]}+ @ ";
todo
- | Slist1sep (symbol,sep) ->
+ | Slist1sep (symbol,sep,false) ->
let todo = visit_symbol symbol todo is_son in
Format.fprintf fmt "{@[<hov2> ";
let todo = visit_symbol sep todo is_son in
diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend
index 25e67131f..119f13093 100644
--- a/helm/software/components/syntax_extensions/.depend
+++ b/helm/software/components/syntax_extensions/.depend
@@ -1,5 +1,5 @@
-utf8Macro.cmi:
-utf8MacroTable.cmo:
-utf8MacroTable.cmx:
-utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
-utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
+utf8Macro.cmi:
+utf8MacroTable.cmo:
+utf8MacroTable.cmx:
+utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
+utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi