# HG changeset patch # User wenzelm # Date 1237472573 -3600 # Node ID ad19c99529eb6c3da943858e5414b1503aabeef6 # Parent 9674f64a07026b27f5e6fe26b5afd95173be227d moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early; diff -r 9674f64a0702 -r ad19c99529eb src/Pure/General/ROOT.ML --- 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"; diff -r 9674f64a0702 -r ad19c99529eb src/Pure/General/antiquote.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 <> "\\" andalso s <> "\\" + 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 --| $$$ "\\" >> Open || + Symbol_Pos.scan_pos --| $$$ "\\" >> 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; diff -r 9674f64a0702 -r ad19c99529eb src/Pure/IsaMakefile --- 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 \ diff -r 9674f64a0702 -r ad19c99529eb src/Pure/Isar/ROOT.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*) diff -r 9674f64a0702 -r ad19c99529eb src/Pure/Isar/antiquote.ML --- 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 <> "\\" andalso s <> "\\" - 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 --| $$$ "\\" >> Open || - Symbol_Pos.scan_pos --| $$$ "\\" >> 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;