--- a/src/Pure/General/ROOT.ML Thu Mar 19 15:22:53 2009 +0100
+++ b/src/Pure/General/ROOT.ML Thu Mar 19 15:22:53 2009 +0100
@@ -15,6 +15,7 @@
use "seq.ML";
use "position.ML";
use "symbol_pos.ML";
+use "antiquote.ML";
use "../ML/ml_lex.ML";
use "../ML/ml_parse.ML";
use "secure.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/antiquote.ML Thu Mar 19 15:22:53 2009 +0100
@@ -0,0 +1,90 @@
+(* Title: Pure/General/antiquote.ML
+ Author: Markus Wenzel, TU Muenchen
+
+Text with antiquotations of inner items (types, terms, theorems etc.).
+*)
+
+signature ANTIQUOTE =
+sig
+ datatype antiquote =
+ Text of string | Antiq of Symbol_Pos.T list * Position.T |
+ Open of Position.T | Close of Position.T
+ val is_antiq: antiquote -> bool
+ val read: Symbol_Pos.T list * Position.T -> antiquote list
+end;
+
+structure Antiquote: ANTIQUOTE =
+struct
+
+(* datatype antiquote *)
+
+datatype antiquote =
+ Text of string |
+ Antiq of Symbol_Pos.T list * Position.T |
+ Open of Position.T |
+ Close of Position.T;
+
+fun is_antiq (Text _) = false
+ | is_antiq _ = true;
+
+
+(* check_nesting *)
+
+fun err_unbalanced pos =
+ error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
+
+fun check_nesting antiqs =
+ let
+ fun check [] [] = ()
+ | check [] (pos :: _) = err_unbalanced pos
+ | check (Open pos :: ants) ps = check ants (pos :: ps)
+ | check (Close pos :: _) [] = err_unbalanced pos
+ | check (Close _ :: ants) (_ :: ps) = check ants ps
+ | check (_ :: ants) ps = check ants ps;
+ in check antiqs [] end;
+
+
+(* scan_antiquote *)
+
+open Basic_Symbol_Pos;
+
+local
+
+val scan_txt =
+ $$$ "@" --| Scan.ahead (~$$$ "{") ||
+ Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
+ andalso Symbol.is_regular s) >> single;
+
+val scan_ant =
+ Symbol_Pos.scan_quoted ||
+ Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
+
+val scan_antiq =
+ Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
+ Symbol_Pos.!!! "missing closing brace of antiquotation"
+ (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
+ >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
+
+in
+
+val scan_antiquote =
+ (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) ||
+ scan_antiq ||
+ Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
+ Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
+
+end;
+
+
+(* read *)
+
+fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
+ | report_antiq _ = ();
+
+fun read ([], _) = []
+ | read (syms, pos) =
+ (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
+ SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
+ | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
+
+end;
--- a/src/Pure/IsaMakefile Thu Mar 19 15:22:53 2009 +0100
+++ b/src/Pure/IsaMakefile Thu Mar 19 15:22:53 2009 +0100
@@ -45,17 +45,17 @@
Concurrent/mailbox.ML Concurrent/par_list.ML \
Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML \
Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML \
- General/alist.ML General/balanced_tree.ML General/basics.ML \
- General/binding.ML General/buffer.ML General/file.ML \
- General/graph.ML General/heap.ML General/integer.ML General/lazy.ML \
- General/long_name.ML General/markup.ML General/name_space.ML \
- General/ord_list.ML General/output.ML General/path.ML \
- General/position.ML General/pretty.ML General/print_mode.ML \
- General/properties.ML General/queue.ML General/scan.ML \
- General/secure.ML General/seq.ML General/source.ML General/stack.ML \
- General/symbol.ML General/symbol_pos.ML General/table.ML \
- General/url.ML General/xml.ML General/yxml.ML Isar/ROOT.ML \
- Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
+ General/alist.ML General/antiquote.ML General/balanced_tree.ML \
+ General/basics.ML General/binding.ML General/buffer.ML \
+ General/file.ML General/graph.ML General/heap.ML General/integer.ML \
+ General/lazy.ML General/long_name.ML General/markup.ML \
+ General/name_space.ML General/ord_list.ML General/output.ML \
+ General/path.ML General/position.ML General/pretty.ML \
+ General/print_mode.ML General/properties.ML General/queue.ML \
+ General/scan.ML General/secure.ML General/seq.ML General/source.ML \
+ General/stack.ML General/symbol.ML General/symbol_pos.ML \
+ General/table.ML General/url.ML General/xml.ML General/yxml.ML \
+ Isar/ROOT.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \
Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML \
Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML \
--- a/src/Pure/Isar/ROOT.ML Thu Mar 19 15:22:53 2009 +0100
+++ b/src/Pure/Isar/ROOT.ML Thu Mar 19 15:22:53 2009 +0100
@@ -24,7 +24,6 @@
use "outer_parse.ML";
use "value_parse.ML";
use "args.ML";
-use "antiquote.ML";
use "../ML/ml_context.ML";
(*theory sources*)
--- a/src/Pure/Isar/antiquote.ML Thu Mar 19 15:22:53 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-(* Title: Pure/Isar/antiquote.ML
- Author: Markus Wenzel, TU Muenchen
-
-Text with antiquotations of inner items (terms, types etc.).
-*)
-
-signature ANTIQUOTE =
-sig
- datatype antiquote =
- Text of string | Antiq of Symbol_Pos.T list * Position.T |
- Open of Position.T | Close of Position.T
- val is_antiq: antiquote -> bool
- val read: Symbol_Pos.T list * Position.T -> antiquote list
- val read_antiq: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
- Symbol_Pos.T list * Position.T -> 'a
-end;
-
-structure Antiquote: ANTIQUOTE =
-struct
-
-(* datatype antiquote *)
-
-datatype antiquote =
- Text of string |
- Antiq of Symbol_Pos.T list * Position.T |
- Open of Position.T |
- Close of Position.T;
-
-fun is_antiq (Text _) = false
- | is_antiq _ = true;
-
-
-(* check_nesting *)
-
-fun err_unbalanced pos =
- error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
-
-fun check_nesting antiqs =
- let
- fun check [] [] = ()
- | check [] (pos :: _) = err_unbalanced pos
- | check (Open pos :: ants) ps = check ants (pos :: ps)
- | check (Close pos :: _) [] = err_unbalanced pos
- | check (Close _ :: ants) (_ :: ps) = check ants ps
- | check (_ :: ants) ps = check ants ps;
- in check antiqs [] end;
-
-
-(* scan_antiquote *)
-
-open Basic_Symbol_Pos;
-structure T = OuterLex;
-
-local
-
-val scan_txt =
- $$$ "@" --| Scan.ahead (~$$$ "{") ||
- Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
- andalso Symbol.is_regular s) >> single;
-
-val scan_ant =
- T.scan_quoted ||
- Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
-
-val scan_antiq =
- Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
- T.!!! "missing closing brace of antiquotation"
- (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
- >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
-
-in
-
-val scan_antiquote =
- (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) ||
- scan_antiq ||
- Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
- Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
-
-end;
-
-
-(* read *)
-
-fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
- | report_antiq _ = ();
-
-fun read ([], _) = []
- | read (syms, pos) =
- (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
- SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
- | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
-
-
-(* read_antiq *)
-
-fun read_antiq lex scan (syms, pos) =
- let
- fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
- "@{" ^ Symbol_Pos.content syms ^ "}");
-
- val res =
- Source.of_list syms
- |> T.source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
- |> T.source_proper
- |> Source.source T.stopper (Scan.error (Scan.bulk scan)) NONE
- |> Source.exhaust;
- in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
-
-end;