# HG changeset patch
# User ballarin
# Date 1228900278 -3600
# Node ID 721529248e31482a6d30fe1bd3db6da85e4ba098
# Parent  ce100fbc3c8ec7604bf19dcd74feee6bf283276a
Enable keyword 'structure' in for clause of locale expression.

diff -r ce100fbc3c8e -r 721529248e31 src/FOL/ex/NewLocaleSetup.thy
--- a/src/FOL/ex/NewLocaleSetup.thy	Mon Dec 08 18:44:24 2008 +0100
+++ b/src/FOL/ex/NewLocaleSetup.thy	Wed Dec 10 10:11:18 2008 +0100
@@ -16,7 +16,7 @@
 val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;
 
 val locale_val =
-  Expression.parse_expression --
+  SpecParse.locale_expression --
     Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
   Scan.repeat1 SpecParse.context_element >> pair ([], []);
 
@@ -42,7 +42,7 @@
 val _ =
   OuterSyntax.command "interpretation"
     "prove interpretation of locale expression in theory" K.thy_goal
-    (P.!!! Expression.parse_expression
+    (P.!!! SpecParse.locale_expression
         >> (fn expr => Toplevel.print o
             Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
 
@@ -50,7 +50,7 @@
   OuterSyntax.command "interpret"
     "prove interpretation of locale expression in proof context"
     (K.tag_proof K.prf_goal)
-    (P.!!! Expression.parse_expression
+    (P.!!! SpecParse.locale_expression
         >> (fn expr => Toplevel.print o
             Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
 
diff -r ce100fbc3c8e -r 721529248e31 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Dec 08 18:44:24 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Wed Dec 10 10:11:18 2008 +0100
@@ -30,10 +30,6 @@
   val interpretation: expression_i -> theory -> Proof.state;
   val interpret_cmd: expression -> bool -> Proof.state -> Proof.state;
   val interpret: expression_i -> bool -> Proof.state -> Proof.state;
-
-  (* Debugging and development *)
-  val parse_expression: OuterParse.token list -> expression * OuterParse.token list
-    (* FIXME to spec_parse.ML *)
 end;
 
 
@@ -55,63 +51,6 @@
 type expression_i = term expr * (Binding.T * typ option * mixfix) list;
 
 
-(** Parsing and printing **)
-
-local
-
-structure P = OuterParse;
-
-val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
-   P.$$$ "defines" || P.$$$ "notes";
-fun plus1_unless test scan =
-  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
-
-val prefix = P.name --| P.$$$ ":";
-val named = P.name -- (P.$$$ "=" |-- P.term);
-val position = P.maybe P.term;
-val instance = P.$$$ "where" |-- P.and_list1 named >> Named ||
-  Scan.repeat1 position >> Positional;
-
-in
-
-val parse_expression =
-  let
-    fun expr2 x = P.xname x;
-    fun expr1 x = (Scan.optional prefix "" -- expr2 --
-      Scan.optional instance (Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
-    fun expr0 x = (plus1_unless loc_keyword expr1) x;
-  in expr0 -- P.for_fixes end;
-
-end;
-
-fun pretty_expr thy expr =
-  let
-    fun pretty_pos NONE = Pretty.str "_"
-      | pretty_pos (SOME x) = Pretty.str x;
-    fun pretty_named (x, y) = [Pretty.str x, Pretty.brk 1, Pretty.str "=",
-          Pretty.brk 1, Pretty.str y] |> Pretty.block;
-    fun pretty_ren (Positional ps) = take_suffix is_none ps |> snd |>
-          map pretty_pos |> Pretty.breaks
-      | pretty_ren (Named []) = []
-      | pretty_ren (Named ps) = Pretty.str "where" :: Pretty.brk 1 ::
-          (ps |> map pretty_named |> Pretty.separate "and");
-    fun pretty_rename (loc, ("", ren)) =
-          Pretty.block (Pretty.str (NewLocale.extern thy loc) :: Pretty.brk 1 :: pretty_ren ren) 
-      | pretty_rename (loc, (prfx, ren)) =
-          Pretty.block (Pretty.str prfx :: Pretty.brk 1 :: Pretty.str (NewLocale.extern thy loc) ::
-            Pretty.brk 1 :: pretty_ren ren);
-  in Pretty.separate "+" (map pretty_rename expr) |> Pretty.block end;
-
-fun err_in_expr thy msg expr =
-  let
-    val err_msg =
-      if null expr then msg
-      else msg ^ "\n" ^ Pretty.string_of (Pretty.block
-        [Pretty.str "The above error(s) occurred in expression:", Pretty.brk 1,
-          pretty_expr thy expr])
-  in error err_msg end;
-
-
 (** Internalise locale names in expr **)
 
 fun intern thy instances =  map (apfst (NewLocale.intern thy)) instances;
diff -r ce100fbc3c8e -r 721529248e31 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Dec 08 18:44:24 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Dec 10 10:11:18 2008 +0100
@@ -401,7 +401,7 @@
 val _ =
   OuterSyntax.command "sublocale"
     "prove sublocale relation between a locale and a locale expression" K.thy_goal
-    (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! Expression.parse_expression
+    (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expression
       >> (fn (loc, expr) =>
         Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr))));
 
diff -r ce100fbc3c8e -r 721529248e31 src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Mon Dec 08 18:44:24 2008 +0100
+++ b/src/Pure/Isar/spec_parse.ML	Wed Dec 10 10:11:18 2008 +0100
@@ -26,6 +26,7 @@
   val locale_insts: token list -> (string option list * (Attrib.binding * string) list) * token list
   val class_expr: token list -> string list * token list
   val locale_expr: token list -> Locale.expr * token list
+  val locale_expression: OuterParse.token list -> Expression.expression * OuterParse.token list
   val locale_keyword: token list -> string * token list
   val context_element: token list -> Element.context * token list
   val statement: token list -> (Attrib.binding * (string * string list) list) list * token list
@@ -103,6 +104,12 @@
 
 val rename = P.name -- Scan.option P.mixfix;
 
+val prefix = P.name --| P.$$$ ":";
+val named = P.name -- (P.$$$ "=" |-- P.term);
+val position = P.maybe P.term;
+val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named ||
+  Scan.repeat1 position >> Expression.Positional;
+
 in
 
 val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
@@ -117,6 +124,14 @@
     and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
   in expr0 end;
 
+val locale_expression =
+  let
+    fun expr2 x = P.xname x;
+    fun expr1 x = (Scan.optional prefix "" -- expr2 --
+      Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
+    fun expr0 x = (plus1_unless locale_keyword expr1) x;
+  in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
+
 val context_element = P.group "context element" loc_element;
 
 end;