# HG changeset patch
# User haftmann
# Date 1284651110 -7200
# Node ID 8866d068791a93a6c0333c167b54c79d6abc4dc3
# Parent  8bc560df99eacf5eb94667c8fb324f9c51b886bd
moved material intro distribution proper

diff -r 8bc560df99ea -r 8866d068791a doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Thu Sep 16 16:51:44 2010 +0200
+++ b/doc-src/more_antiquote.ML	Thu Sep 16 17:31:50 2010 +0200
@@ -6,47 +6,11 @@
 
 signature MORE_ANTIQUOTE =
 sig
-  val typewriter: string -> string
 end;
 
 structure More_Antiquote : MORE_ANTIQUOTE =
 struct
 
-(* printing typewriter lines *)
-
-fun typewriter s =
-  let
-    val parse = Scan.repeat
-      (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
-        || (Scan.this_string " "
-          || Scan.this_string "."
-          || Scan.this_string ","
-          || Scan.this_string ":"
-          || Scan.this_string ";"
-          || Scan.this_string "\"" |-- Scan.succeed "{\\char34}"
-          || Scan.this_string "#" |-- Scan.succeed "{\\char35}"
-          || Scan.this_string "$" |-- Scan.succeed "{\\char36}"
-          || Scan.this_string "%" |-- Scan.succeed "{\\char37}"
-          || Scan.this_string "&" |-- Scan.succeed "{\\char38}"
-          || Scan.this_string "\\" |-- Scan.succeed "{\\char92}"
-          || Scan.this_string "^" |-- Scan.succeed "{\\char94}"
-          || Scan.this_string "_" |-- Scan.succeed "{\\char95}"
-          || Scan.this_string "{" |-- Scan.succeed "{\\char123}"
-          || Scan.this_string "}" |-- Scan.succeed "{\\char125}"
-          || Scan.this_string "~" |-- Scan.succeed "{\\char126}")
-          -- Scan.repeat (Scan.this_string " ")
-          >> (fn (x, xs) => x ^ replicate_string (length xs) "~")
-        || Scan.one Symbol.not_eof);
-    fun is_newline s = (s = "\n");
-    val cs = explode s |> take_prefix is_newline |> snd
-      |> take_suffix is_newline |> fst;
-    val (texts, []) =  Scan.finite Symbol.stopper parse cs
-  in if null texts
-    then ""
-    else implode ("\\isatypewriter%\n\\noindent%\n\\hspace*{0pt}" :: texts)
-  end
-
-
 (* code theorem antiquotation *)
 
 local
@@ -81,36 +45,4 @@
 
 end;
 
-
-(* code antiquotation *)
-
-local
-
-  val parse_const_terms = Scan.repeat1 Args.term
-    >> (fn ts => fn thy => map (Code.check_const thy) ts);
-  val parse_consts = Scan.lift (Args.parens (Args.$$$ "consts")) |-- parse_const_terms
-    >> (fn mk_cs => fn thy => fn naming => map_filter (Code_Thingol.lookup_const naming) (mk_cs thy));
-  val parse_types = Scan.lift (Args.parens (Args.$$$ "types") |-- Scan.repeat1 Args.name)
-    >> (fn tycos => fn thy => fn naming => map_filter (Code_Thingol.lookup_tyco naming o Sign.intern_type thy) tycos);
-  val parse_classes = Scan.lift (Args.parens (Args.$$$ "classes") |-- Scan.repeat1 Args.name)
-    >> (fn classes => fn thy => fn naming => map_filter (Code_Thingol.lookup_class naming o Sign.intern_class thy) classes);
-  val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name))
-    >> (fn insts => fn thy => fn naming => map_filter (Code_Thingol.lookup_instance naming o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts);
-  val parse_names = parse_consts || parse_types || parse_classes || parse_instances;
-
-in
-
-val _ = Thy_Output.antiquotation "code_stmts"
-  (parse_const_terms -- Scan.repeat parse_names
-    -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int)))
-  (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) =>
-    let val thy = ProofContext.theory_of ctxt in
-      Code_Target.present_code thy (mk_cs thy)
-        (fn naming => maps (fn f => f thy naming) mk_stmtss)
-        target some_width "Example" []
-      |> typewriter
-    end);
-
 end;
-
-end;