src/Tools/value.ML
changeset 36960 01594f816e3a
parent 33522 737589bb9bb8
child 37146 f652333bbf8e
     1.1 --- a/src/Tools/value.ML	Mon May 17 15:11:25 2010 +0200
     1.2 +++ b/src/Tools/value.ML	Mon May 17 23:54:15 2010 +0200
     1.3 @@ -52,15 +52,13 @@
     1.4          Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
     1.5    in Pretty.writeln p end;
     1.6  
     1.7 -local structure P = OuterParse and K = OuterKeyword in
     1.8 -
     1.9 -val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
    1.10 +val opt_modes =
    1.11 +  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
    1.12  
    1.13 -val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag
    1.14 -  (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term
    1.15 -    >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
    1.16 -        (value_cmd some_name modes t)));
    1.17 -
    1.18 -end; (*local*)
    1.19 +val _ =
    1.20 +  Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag
    1.21 +    (Scan.option (Parse.$$$ "[" |-- Parse.xname --| Parse.$$$ "]") -- opt_modes -- Parse.term
    1.22 +      >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
    1.23 +          (value_cmd some_name modes t)));
    1.24  
    1.25  end;