src/Pure/Isar/expression.ML
changeset 29033 721529248e31
parent 29021 ce100fbc3c8e
child 29034 3dc51c01f9f3
     1.1 --- a/src/Pure/Isar/expression.ML	Mon Dec 08 18:44:24 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Dec 10 10:11:18 2008 +0100
     1.3 @@ -30,10 +30,6 @@
     1.4    val interpretation: expression_i -> theory -> Proof.state;
     1.5    val interpret_cmd: expression -> bool -> Proof.state -> Proof.state;
     1.6    val interpret: expression_i -> bool -> Proof.state -> Proof.state;
     1.7 -
     1.8 -  (* Debugging and development *)
     1.9 -  val parse_expression: OuterParse.token list -> expression * OuterParse.token list
    1.10 -    (* FIXME to spec_parse.ML *)
    1.11  end;
    1.12  
    1.13  
    1.14 @@ -55,63 +51,6 @@
    1.15  type expression_i = term expr * (Binding.T * typ option * mixfix) list;
    1.16  
    1.17  
    1.18 -(** Parsing and printing **)
    1.19 -
    1.20 -local
    1.21 -
    1.22 -structure P = OuterParse;
    1.23 -
    1.24 -val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
    1.25 -   P.$$$ "defines" || P.$$$ "notes";
    1.26 -fun plus1_unless test scan =
    1.27 -  scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
    1.28 -
    1.29 -val prefix = P.name --| P.$$$ ":";
    1.30 -val named = P.name -- (P.$$$ "=" |-- P.term);
    1.31 -val position = P.maybe P.term;
    1.32 -val instance = P.$$$ "where" |-- P.and_list1 named >> Named ||
    1.33 -  Scan.repeat1 position >> Positional;
    1.34 -
    1.35 -in
    1.36 -
    1.37 -val parse_expression =
    1.38 -  let
    1.39 -    fun expr2 x = P.xname x;
    1.40 -    fun expr1 x = (Scan.optional prefix "" -- expr2 --
    1.41 -      Scan.optional instance (Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
    1.42 -    fun expr0 x = (plus1_unless loc_keyword expr1) x;
    1.43 -  in expr0 -- P.for_fixes end;
    1.44 -
    1.45 -end;
    1.46 -
    1.47 -fun pretty_expr thy expr =
    1.48 -  let
    1.49 -    fun pretty_pos NONE = Pretty.str "_"
    1.50 -      | pretty_pos (SOME x) = Pretty.str x;
    1.51 -    fun pretty_named (x, y) = [Pretty.str x, Pretty.brk 1, Pretty.str "=",
    1.52 -          Pretty.brk 1, Pretty.str y] |> Pretty.block;
    1.53 -    fun pretty_ren (Positional ps) = take_suffix is_none ps |> snd |>
    1.54 -          map pretty_pos |> Pretty.breaks
    1.55 -      | pretty_ren (Named []) = []
    1.56 -      | pretty_ren (Named ps) = Pretty.str "where" :: Pretty.brk 1 ::
    1.57 -          (ps |> map pretty_named |> Pretty.separate "and");
    1.58 -    fun pretty_rename (loc, ("", ren)) =
    1.59 -          Pretty.block (Pretty.str (NewLocale.extern thy loc) :: Pretty.brk 1 :: pretty_ren ren) 
    1.60 -      | pretty_rename (loc, (prfx, ren)) =
    1.61 -          Pretty.block (Pretty.str prfx :: Pretty.brk 1 :: Pretty.str (NewLocale.extern thy loc) ::
    1.62 -            Pretty.brk 1 :: pretty_ren ren);
    1.63 -  in Pretty.separate "+" (map pretty_rename expr) |> Pretty.block end;
    1.64 -
    1.65 -fun err_in_expr thy msg expr =
    1.66 -  let
    1.67 -    val err_msg =
    1.68 -      if null expr then msg
    1.69 -      else msg ^ "\n" ^ Pretty.string_of (Pretty.block
    1.70 -        [Pretty.str "The above error(s) occurred in expression:", Pretty.brk 1,
    1.71 -          pretty_expr thy expr])
    1.72 -  in error err_msg end;
    1.73 -
    1.74 -
    1.75  (** Internalise locale names in expr **)
    1.76  
    1.77  fun intern thy instances =  map (apfst (NewLocale.intern thy)) instances;