From 12330e6f63404c236614070b32a10b146f9b8a04 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Mon, 15 Apr 2013 13:33:29 +0000
Subject: More functional implementation of locality_flag and program_mode

This commit introduces 2 new vernac_expr constructors:
- VernacLocal (b,v)  that represents a vernacular v with the "Local" modifier
- VernacProgram v    that represents a vernacular v with the "Program" modifier

This allows the parser to avoid using side effects to model the two
modifiers, that are now represented in the AST.  This also decouples the
parsing phase from the interpretation phase, since parsing a second
phrase does not alter the locality flag for the first phrase.

As a consequence all the locality_flag components of vernac_expr have
been removed, but for the ones that (for retro compatibility) allow
an "infix" Local flag.  In these cases the boolean is renamed
obsolete_locality (as the grammar entry that parses it), and during
interpretation we check that at most one locality flag is specified,
using the idiom (where the input local is the obsolete one):

  let local = enforce_XXX_locality locality local in

Another improvement is that the default locality is not chosen in the
parser, but in the interpreter where the idiom

  let local = make_XXX_locality locality in

is used to default the locality to XXX (module/section/whatever).

Unfortunately not all side effects have been removed:
- Flags.program_mode is still used to signal that we are in program mode
- Locality.LocalityFixme.* functions are used in commands that do not
  have an AST, but are parsed as VernacExtend (see vernacinterp.ml)

I guess one could fix the latter case systematically adding an extra
argument "locality" to commands attached using VERNAC COMMAND EXTEND.

Fixing plugins adding commands that honour "Local" should look like this:

 VERNAC COMMAND EXTEND Set_Solver
 | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
     set_default_tactic
-      (Locality.use_section_locality ())
+      (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
       (Tacintern.glob_tactic t) ]
 END

In any case the side effects are set/consumed within then interpretation
phase, and not set during the parsing phase and consumed during the
interpretation phase.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16396 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/flags.ml  | 5 -----
 lib/flags.mli | 5 -----
 2 files changed, 10 deletions(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index bd31b40248..6c67cb237f 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -84,11 +84,6 @@ let auto_intros = ref true
 let make_auto_intros flag = auto_intros := flag
 let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros
 
-(** [program_cmd] indicates that the current command is a Program one.
-    [program_mode] tells that Program mode has been activated, either
-    globally via [Set Program] or locally via the Program command prefix. *)
-
-let program_cmd = ref false
 let program_mode = ref false
 let is_program_mode () = !program_mode
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 6b26c50d9e..6325d7cd44 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -52,11 +52,6 @@ val is_auto_intros : unit -> bool
 val make_term_color : bool -> unit
 val is_term_color : unit -> bool
 
-(** [program_cmd] indicates that the current command is a Program one.
-    [program_mode] tells that Program mode has been activated, either
-    globally via [Set Program] or locally via the Program command prefix. *)
-
-val program_cmd : bool ref
 val program_mode : bool ref
 val is_program_mode : unit -> bool
 
-- 
cgit v1.2.3