1.1 --- a/src/Pure/IsaMakefile Sat May 15 23:16:32 2010 +0200
1.2 +++ b/src/Pure/IsaMakefile Sat May 15 23:23:45 2010 +0200
1.3 @@ -68,15 +68,15 @@
1.4 Isar/isar_syn.ML Isar/keyword.ML Isar/local_defs.ML \
1.5 Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \
1.6 Isar/method.ML Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML \
1.7 - Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML Isar/proof.ML \
1.8 - Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
1.9 - Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML \
1.10 - Isar/skip_proof.ML Isar/spec_parse.ML Isar/spec_rules.ML \
1.11 - Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \
1.12 - Isar/typedecl.ML Isar/value_parse.ML ML/ml_antiquote.ML \
1.13 - ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML \
1.14 - ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
1.15 - ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
1.16 + Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML \
1.17 + Isar/parse_value.ML Isar/proof.ML Isar/proof_context.ML \
1.18 + Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
1.19 + Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML \
1.20 + Isar/spec_parse.ML Isar/spec_rules.ML Isar/specification.ML \
1.21 + Isar/theory_target.ML Isar/toplevel.ML Isar/typedecl.ML \
1.22 + ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML \
1.23 + ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML \
1.24 + ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
1.25 ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \
1.26 Proof/extraction.ML Proof/proof_rewrite_rules.ML \
1.27 Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
2.1 --- a/src/Pure/Isar/isar_document.ML Sat May 15 23:16:32 2010 +0200
2.2 +++ b/src/Pure/Isar/isar_document.ML Sat May 15 23:23:45 2010 +0200
2.3 @@ -275,8 +275,6 @@
2.4
2.5 (** concrete syntax **)
2.6
2.7 -local structure V = ValueParse in
2.8 -
2.9 val _ =
2.10 OuterSyntax.internal_command "Isar.define_command"
2.11 (Parse.string -- Parse.string >> (fn (id, text) =>
2.12 @@ -296,12 +294,10 @@
2.13 val _ =
2.14 OuterSyntax.internal_command "Isar.edit_document"
2.15 (Parse.string -- Parse.string --
2.16 - V.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE)
2.17 + Parse_Value.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE)
2.18 >> (fn ((id, new_id), edits) =>
2.19 Toplevel.position (Position.id_only new_id) o
2.20 Toplevel.imperative (fn () => edit_document id new_id edits)));
2.21
2.22 end;
2.23
2.24 -end;
2.25 -
3.1 --- a/src/Pure/Isar/isar_syn.ML Sat May 15 23:16:32 2010 +0200
3.2 +++ b/src/Pure/Isar/isar_syn.ML Sat May 15 23:23:45 2010 +0200
3.3 @@ -773,7 +773,7 @@
3.4 (* nested commands *)
3.5
3.6 val props_text =
3.7 - Scan.optional ValueParse.properties [] -- Parse.position Parse.string
3.8 + Scan.optional Parse_Value.properties [] -- Parse.position Parse.string
3.9 >> (fn (props, (str, pos)) =>
3.10 (Position.of_properties (Position.default_properties pos props), str));
3.11
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Pure/Isar/parse_value.ML Sat May 15 23:23:45 2010 +0200
4.3 @@ -0,0 +1,42 @@
4.4 +(* Title: Pure/Isar/parse_value.ML
4.5 + Author: Makarius
4.6 +
4.7 +Outer syntax parsers for basic ML values.
4.8 +*)
4.9 +
4.10 +signature PARSE_VALUE =
4.11 +sig
4.12 + val comma: 'a parser -> 'a parser
4.13 + val equal: 'a parser -> 'a parser
4.14 + val parens: 'a parser -> 'a parser
4.15 + val unit: unit parser
4.16 + val pair: 'a parser -> 'b parser -> ('a * 'b) parser
4.17 + val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
4.18 + val list: 'a parser -> 'a list parser
4.19 + val properties: Properties.T parser
4.20 +end;
4.21 +
4.22 +structure Parse_Value: PARSE_VALUE =
4.23 +struct
4.24 +
4.25 +(* syntax utilities *)
4.26 +
4.27 +fun comma p = Parse.$$$ "," |-- Parse.!!! p;
4.28 +fun equal p = Parse.$$$ "=" |-- Parse.!!! p;
4.29 +fun parens p = Parse.$$$ "(" |-- Parse.!!! (p --| Parse.$$$ ")");
4.30 +
4.31 +
4.32 +(* tuples *)
4.33 +
4.34 +val unit = parens (Scan.succeed ());
4.35 +fun pair p1 p2 = parens (p1 -- comma p2);
4.36 +fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> Parse.triple1;
4.37 +
4.38 +
4.39 +(* lists *)
4.40 +
4.41 +fun list p = parens (Parse.enum "," p);
4.42 +val properties = list (Parse.string -- equal Parse.string);
4.43 +
4.44 +end;
4.45 +
5.1 --- a/src/Pure/Isar/value_parse.ML Sat May 15 23:16:32 2010 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,42 +0,0 @@
5.4 -(* Title: Pure/Isar/value_parse.ML
5.5 - Author: Makarius
5.6 -
5.7 -Outer syntax parsers for basic ML values.
5.8 -*)
5.9 -
5.10 -signature VALUE_PARSE =
5.11 -sig
5.12 - val comma: 'a parser -> 'a parser
5.13 - val equal: 'a parser -> 'a parser
5.14 - val parens: 'a parser -> 'a parser
5.15 - val unit: unit parser
5.16 - val pair: 'a parser -> 'b parser -> ('a * 'b) parser
5.17 - val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
5.18 - val list: 'a parser -> 'a list parser
5.19 - val properties: Properties.T parser
5.20 -end;
5.21 -
5.22 -structure ValueParse: VALUE_PARSE =
5.23 -struct
5.24 -
5.25 -(* syntax utilities *)
5.26 -
5.27 -fun comma p = Parse.$$$ "," |-- Parse.!!! p;
5.28 -fun equal p = Parse.$$$ "=" |-- Parse.!!! p;
5.29 -fun parens p = Parse.$$$ "(" |-- Parse.!!! (p --| Parse.$$$ ")");
5.30 -
5.31 -
5.32 -(* tuples *)
5.33 -
5.34 -val unit = parens (Scan.succeed ());
5.35 -fun pair p1 p2 = parens (p1 -- comma p2);
5.36 -fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> Parse.triple1;
5.37 -
5.38 -
5.39 -(* lists *)
5.40 -
5.41 -fun list p = parens (Parse.enum "," p);
5.42 -val properties = list (Parse.string -- equal Parse.string);
5.43 -
5.44 -end;
5.45 -
6.1 --- a/src/Pure/ROOT.ML Sat May 15 23:16:32 2010 +0200
6.2 +++ b/src/Pure/ROOT.ML Sat May 15 23:23:45 2010 +0200
6.3 @@ -170,7 +170,7 @@
6.4 use "Isar/outer_lex.ML";
6.5 use "Isar/keyword.ML";
6.6 use "Isar/parse.ML";
6.7 -use "Isar/value_parse.ML";
6.8 +use "Isar/parse_value.ML";
6.9 use "Isar/args.ML";
6.10
6.11 (*ML support*)