moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
authorwenzelm
Thu Mar 19 15:22:53 2009 +0100 (2009-03-19)
changeset 30587ad19c99529eb
parent 30586 9674f64a0702
child 30588 05f81bbb2614
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
src/Pure/General/ROOT.ML
src/Pure/General/antiquote.ML
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/antiquote.ML
     1.1 --- a/src/Pure/General/ROOT.ML	Thu Mar 19 15:22:53 2009 +0100
     1.2 +++ b/src/Pure/General/ROOT.ML	Thu Mar 19 15:22:53 2009 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4  use "seq.ML";
     1.5  use "position.ML";
     1.6  use "symbol_pos.ML";
     1.7 +use "antiquote.ML";
     1.8  use "../ML/ml_lex.ML";
     1.9  use "../ML/ml_parse.ML";
    1.10  use "secure.ML";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/General/antiquote.ML	Thu Mar 19 15:22:53 2009 +0100
     2.3 @@ -0,0 +1,90 @@
     2.4 +(*  Title:      Pure/General/antiquote.ML
     2.5 +    Author:     Markus Wenzel, TU Muenchen
     2.6 +
     2.7 +Text with antiquotations of inner items (types, terms, theorems etc.).
     2.8 +*)
     2.9 +
    2.10 +signature ANTIQUOTE =
    2.11 +sig
    2.12 +  datatype antiquote =
    2.13 +    Text of string | Antiq of Symbol_Pos.T list * Position.T |
    2.14 +    Open of Position.T | Close of Position.T
    2.15 +  val is_antiq: antiquote -> bool
    2.16 +  val read: Symbol_Pos.T list * Position.T -> antiquote list
    2.17 +end;
    2.18 +
    2.19 +structure Antiquote: ANTIQUOTE =
    2.20 +struct
    2.21 +
    2.22 +(* datatype antiquote *)
    2.23 +
    2.24 +datatype antiquote =
    2.25 +  Text of string |
    2.26 +  Antiq of Symbol_Pos.T list * Position.T |
    2.27 +  Open of Position.T |
    2.28 +  Close of Position.T;
    2.29 +
    2.30 +fun is_antiq (Text _) = false
    2.31 +  | is_antiq _ = true;
    2.32 +
    2.33 +
    2.34 +(* check_nesting *)
    2.35 +
    2.36 +fun err_unbalanced pos =
    2.37 +  error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
    2.38 +
    2.39 +fun check_nesting antiqs =
    2.40 +  let
    2.41 +    fun check [] [] = ()
    2.42 +      | check [] (pos :: _) = err_unbalanced pos
    2.43 +      | check (Open pos :: ants) ps = check ants (pos :: ps)
    2.44 +      | check (Close pos :: _) [] = err_unbalanced pos
    2.45 +      | check (Close _ :: ants) (_ :: ps) = check ants ps
    2.46 +      | check (_ :: ants) ps = check ants ps;
    2.47 +  in check antiqs [] end;
    2.48 +
    2.49 +
    2.50 +(* scan_antiquote *)
    2.51 +
    2.52 +open Basic_Symbol_Pos;
    2.53 +
    2.54 +local
    2.55 +
    2.56 +val scan_txt =
    2.57 +  $$$ "@" --| Scan.ahead (~$$$ "{") ||
    2.58 +  Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
    2.59 +    andalso Symbol.is_regular s) >> single;
    2.60 +
    2.61 +val scan_ant =
    2.62 +  Symbol_Pos.scan_quoted ||
    2.63 +  Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
    2.64 +
    2.65 +val scan_antiq =
    2.66 +  Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
    2.67 +    Symbol_Pos.!!! "missing closing brace of antiquotation"
    2.68 +      (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
    2.69 +  >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
    2.70 +
    2.71 +in
    2.72 +
    2.73 +val scan_antiquote =
    2.74 + (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) ||
    2.75 +  scan_antiq ||
    2.76 +  Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
    2.77 +  Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
    2.78 +
    2.79 +end;
    2.80 +
    2.81 +
    2.82 +(* read *)
    2.83 +
    2.84 +fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
    2.85 +  | report_antiq _ = ();
    2.86 +
    2.87 +fun read ([], _) = []
    2.88 +  | read (syms, pos) =
    2.89 +      (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
    2.90 +        SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
    2.91 +      | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
    2.92 +
    2.93 +end;
     3.1 --- a/src/Pure/IsaMakefile	Thu Mar 19 15:22:53 2009 +0100
     3.2 +++ b/src/Pure/IsaMakefile	Thu Mar 19 15:22:53 2009 +0100
     3.3 @@ -45,17 +45,17 @@
     3.4    Concurrent/mailbox.ML Concurrent/par_list.ML				\
     3.5    Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML		\
     3.6    Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML	\
     3.7 -  General/alist.ML General/balanced_tree.ML General/basics.ML		\
     3.8 -  General/binding.ML General/buffer.ML General/file.ML			\
     3.9 -  General/graph.ML General/heap.ML General/integer.ML General/lazy.ML	\
    3.10 -  General/long_name.ML General/markup.ML General/name_space.ML		\
    3.11 -  General/ord_list.ML General/output.ML General/path.ML			\
    3.12 -  General/position.ML General/pretty.ML General/print_mode.ML		\
    3.13 -  General/properties.ML General/queue.ML General/scan.ML		\
    3.14 -  General/secure.ML General/seq.ML General/source.ML General/stack.ML	\
    3.15 -  General/symbol.ML General/symbol_pos.ML General/table.ML		\
    3.16 -  General/url.ML General/xml.ML General/yxml.ML Isar/ROOT.ML		\
    3.17 -  Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML	\
    3.18 +  General/alist.ML General/antiquote.ML General/balanced_tree.ML	\
    3.19 +  General/basics.ML General/binding.ML General/buffer.ML		\
    3.20 +  General/file.ML General/graph.ML General/heap.ML General/integer.ML	\
    3.21 +  General/lazy.ML General/long_name.ML General/markup.ML		\
    3.22 +  General/name_space.ML General/ord_list.ML General/output.ML		\
    3.23 +  General/path.ML General/position.ML General/pretty.ML			\
    3.24 +  General/print_mode.ML General/properties.ML General/queue.ML		\
    3.25 +  General/scan.ML General/secure.ML General/seq.ML General/source.ML	\
    3.26 +  General/stack.ML General/symbol.ML General/symbol_pos.ML		\
    3.27 +  General/table.ML General/url.ML General/xml.ML General/yxml.ML	\
    3.28 +  Isar/ROOT.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML		\
    3.29    Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML	\
    3.30    Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML		\
    3.31    Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML			\
     4.1 --- a/src/Pure/Isar/ROOT.ML	Thu Mar 19 15:22:53 2009 +0100
     4.2 +++ b/src/Pure/Isar/ROOT.ML	Thu Mar 19 15:22:53 2009 +0100
     4.3 @@ -24,7 +24,6 @@
     4.4  use "outer_parse.ML";
     4.5  use "value_parse.ML";
     4.6  use "args.ML";
     4.7 -use "antiquote.ML";
     4.8  use "../ML/ml_context.ML";
     4.9  
    4.10  (*theory sources*)
     5.1 --- a/src/Pure/Isar/antiquote.ML	Thu Mar 19 15:22:53 2009 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,109 +0,0 @@
     5.4 -(*  Title:      Pure/Isar/antiquote.ML
     5.5 -    Author:     Markus Wenzel, TU Muenchen
     5.6 -
     5.7 -Text with antiquotations of inner items (terms, types etc.).
     5.8 -*)
     5.9 -
    5.10 -signature ANTIQUOTE =
    5.11 -sig
    5.12 -  datatype antiquote =
    5.13 -    Text of string | Antiq of Symbol_Pos.T list * Position.T |
    5.14 -    Open of Position.T | Close of Position.T
    5.15 -  val is_antiq: antiquote -> bool
    5.16 -  val read: Symbol_Pos.T list * Position.T -> antiquote list
    5.17 -  val read_antiq: Scan.lexicon -> (OuterLex.token list -> 'a * OuterLex.token list) ->
    5.18 -    Symbol_Pos.T list * Position.T -> 'a
    5.19 -end;
    5.20 -
    5.21 -structure Antiquote: ANTIQUOTE =
    5.22 -struct
    5.23 -
    5.24 -(* datatype antiquote *)
    5.25 -
    5.26 -datatype antiquote =
    5.27 -  Text of string |
    5.28 -  Antiq of Symbol_Pos.T list * Position.T |
    5.29 -  Open of Position.T |
    5.30 -  Close of Position.T;
    5.31 -
    5.32 -fun is_antiq (Text _) = false
    5.33 -  | is_antiq _ = true;
    5.34 -
    5.35 -
    5.36 -(* check_nesting *)
    5.37 -
    5.38 -fun err_unbalanced pos =
    5.39 -  error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos);
    5.40 -
    5.41 -fun check_nesting antiqs =
    5.42 -  let
    5.43 -    fun check [] [] = ()
    5.44 -      | check [] (pos :: _) = err_unbalanced pos
    5.45 -      | check (Open pos :: ants) ps = check ants (pos :: ps)
    5.46 -      | check (Close pos :: _) [] = err_unbalanced pos
    5.47 -      | check (Close _ :: ants) (_ :: ps) = check ants ps
    5.48 -      | check (_ :: ants) ps = check ants ps;
    5.49 -  in check antiqs [] end;
    5.50 -
    5.51 -
    5.52 -(* scan_antiquote *)
    5.53 -
    5.54 -open Basic_Symbol_Pos;
    5.55 -structure T = OuterLex;
    5.56 -
    5.57 -local
    5.58 -
    5.59 -val scan_txt =
    5.60 -  $$$ "@" --| Scan.ahead (~$$$ "{") ||
    5.61 -  Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>"
    5.62 -    andalso Symbol.is_regular s) >> single;
    5.63 -
    5.64 -val scan_ant =
    5.65 -  T.scan_quoted ||
    5.66 -  Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single;
    5.67 -
    5.68 -val scan_antiq =
    5.69 -  Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
    5.70 -    T.!!! "missing closing brace of antiquotation"
    5.71 -      (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
    5.72 -  >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2)));
    5.73 -
    5.74 -in
    5.75 -
    5.76 -val scan_antiquote =
    5.77 - (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) ||
    5.78 -  scan_antiq ||
    5.79 -  Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
    5.80 -  Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
    5.81 -
    5.82 -end;
    5.83 -
    5.84 -
    5.85 -(* read *)
    5.86 -
    5.87 -fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos
    5.88 -  | report_antiq _ = ();
    5.89 -
    5.90 -fun read ([], _) = []
    5.91 -  | read (syms, pos) =
    5.92 -      (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
    5.93 -        SOME xs => (List.app report_antiq xs; check_nesting xs; xs)
    5.94 -      | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
    5.95 -
    5.96 -
    5.97 -(* read_antiq *)
    5.98 -
    5.99 -fun read_antiq lex scan (syms, pos) =
   5.100 -  let
   5.101 -    fun err msg = cat_error msg ("Malformed antiquotation" ^ Position.str_of pos ^ ":\n" ^
   5.102 -      "@{" ^ Symbol_Pos.content syms ^ "}");
   5.103 -
   5.104 -    val res =
   5.105 -      Source.of_list syms
   5.106 -      |> T.source' {do_recover = NONE} (K (lex, Scan.empty_lexicon))
   5.107 -      |> T.source_proper
   5.108 -      |> Source.source T.stopper (Scan.error (Scan.bulk scan)) NONE
   5.109 -      |> Source.exhaust;
   5.110 -  in (case res of [x] => x | _ => err "") handle ERROR msg => err msg end;
   5.111 -
   5.112 -end;