moved @{ML_functor} and @{ML_text} to Pure;
authorwenzelm
Mon Mar 09 20:34:11 2009 +0100 (2009-03-09)
changeset 30394c11a1e65a2ed
parent 30393 aa6f42252bf6
child 30395 f3103bd2b167
moved @{ML_functor} and @{ML_text} to Pure;
adapted to simplified ThyOutput.antiquotation interface;
misc tuning;
doc-src/antiquote_setup.ML
doc-src/more_antiquote.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/doc-src/antiquote_setup.ML	Mon Mar 09 20:29:45 2009 +0100
     1.2 +++ b/doc-src/antiquote_setup.ML	Mon Mar 09 20:34:11 2009 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      Doc/antiquote_setup.ML
     1.5 +(*  Title:      doc-src/antiquote_setup.ML
     1.6      Author:     Makarius
     1.7  
     1.8  Auxiliary antiquotations for the Isabelle manuals.
     1.9 @@ -52,87 +52,70 @@
    1.10  fun ml_exn (txt1, "") = "fn _ => (" ^ txt1 ^ ": exn);"
    1.11    | ml_exn (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ " -> exn);";
    1.12  
    1.13 -fun ml_structure (txt, _) = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
    1.14 +fun ml_structure (txt, _) = "functor XXX() = struct structure XX = " ^ txt ^ " end;";
    1.15  
    1.16 -fun ml_functor _ = "val _ = ();";  (*no check!*)
    1.17 +fun ml_functor _ = "";  (*no check!*)
    1.18  
    1.19 -fun index_ml kind ml src ctxt (txt1, txt2) =
    1.20 -  let
    1.21 -    val txt = if txt2 = "" then txt1 else
    1.22 -      if kind = "type" then txt1 ^ " = " ^ txt2
    1.23 -      else if kind = "exception" then txt1 ^ " of " ^ txt2
    1.24 -      else txt1 ^ ": " ^ txt2;
    1.25 -    val txt' = if kind = "" then txt else kind ^ " " ^ txt;
    1.26 -    val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
    1.27 -    val kind' = if kind = "" then "ML" else "ML " ^ kind;
    1.28 -  in
    1.29 -    "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
    1.30 -    (txt'
    1.31 -    |> (if ! ThyOutput.quotes then quote else I)
    1.32 -    |> (if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.33 -        else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
    1.34 -  end;
    1.35 -
    1.36 -fun output_ml ctxt src =
    1.37 -  if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.38 -  else
    1.39 -    split_lines
    1.40 -    #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
    1.41 -    #> space_implode "\\isasep\\isanewline%\n";
    1.42 -
    1.43 -fun ml_args x = ThyOutput.args (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) x;
    1.44 +fun index_ml name kind ml = ThyOutput.antiquotation name
    1.45 +  (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) ""))
    1.46 +  (fn {context = ctxt, ...} => fn (txt1, txt2) =>
    1.47 +    let
    1.48 +      val txt =
    1.49 +        if txt2 = "" then txt1
    1.50 +        else if kind = "type" then txt1 ^ " = " ^ txt2
    1.51 +        else if kind = "exception" then txt1 ^ " of " ^ txt2
    1.52 +        else txt1 ^ ": " ^ txt2;
    1.53 +      val txt' = if kind = "" then txt else kind ^ " " ^ txt;
    1.54 +      val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
    1.55 +      val kind' = if kind = "" then "ML" else "ML " ^ kind;
    1.56 +    in
    1.57 +      "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
    1.58 +      (txt'
    1.59 +      |> (if ! ThyOutput.quotes then quote else I)
    1.60 +      |> (if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.61 +          else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
    1.62 +    end);
    1.63  
    1.64  in
    1.65  
    1.66 -val _ = ThyOutput.add_commands
    1.67 - [("index_ML", ml_args (index_ml "" ml_val)),
    1.68 -  ("index_ML_type", ml_args (index_ml "type" ml_type)),
    1.69 -  ("index_ML_exn", ml_args (index_ml "exception" ml_exn)),
    1.70 -  ("index_ML_structure", ml_args (index_ml "structure" ml_structure)),
    1.71 -  ("index_ML_functor", ml_args (index_ml "functor" ml_functor)),
    1.72 -  ("ML_functor", ThyOutput.args (Scan.lift Args.name) output_ml),
    1.73 -  ("ML_text", ThyOutput.args (Scan.lift Args.name) output_ml)];
    1.74 +val _ = index_ml "index_ML" "" ml_val;
    1.75 +val _ = index_ml "index_ML_type" "type" ml_type;
    1.76 +val _ = index_ml "index_ML_exn" "exception" ml_exn;
    1.77 +val _ = index_ml "index_ML_structure" "structure" ml_structure;
    1.78 +val _ = index_ml "index_ML_functor" "functor" ml_functor;
    1.79  
    1.80  end;
    1.81  
    1.82  
    1.83 -(* theorems with names *)
    1.84 -
    1.85 -local
    1.86 +(* named theorems *)
    1.87  
    1.88 -fun output_named_thms src ctxt xs =
    1.89 -  map (apfst (ThyOutput.pretty_thm ctxt)) xs        (*always pretty in order to exhibit errors!*)
    1.90 -  |> (if ! ThyOutput.quotes then map (apfst Pretty.quote) else I)
    1.91 -  |> (if ! ThyOutput.display then
    1.92 -    map (fn (p, name) =>
    1.93 -      Output.output (Pretty.string_of (Pretty.indent (! ThyOutput.indent) p)) ^
    1.94 -      "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
    1.95 -    #> space_implode "\\par\\smallskip%\n"
    1.96 -    #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.97 -  else
    1.98 -    map (fn (p, name) =>
    1.99 -      Output.output (Pretty.str_of p) ^
   1.100 -      "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
   1.101 -    #> space_implode "\\par\\smallskip%\n"
   1.102 -    #> enclose "\\isa{" "}");
   1.103 -
   1.104 -in
   1.105 -
   1.106 -val _ = ThyOutput.add_commands
   1.107 - [("named_thms", ThyOutput.args (Scan.repeat (Attrib.thm --
   1.108 -      Scan.lift (Args.parens Args.name))) output_named_thms)];
   1.109 -
   1.110 -end;
   1.111 +val _ = ThyOutput.antiquotation "named_thms"
   1.112 +  (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
   1.113 +  (fn {context = ctxt, ...} =>
   1.114 +    map (apfst (ThyOutput.pretty_thm ctxt))
   1.115 +    #> (if ! ThyOutput.quotes then map (apfst Pretty.quote) else I)
   1.116 +    #> (if ! ThyOutput.display
   1.117 +        then
   1.118 +          map (fn (p, name) =>
   1.119 +            Output.output (Pretty.string_of (Pretty.indent (! ThyOutput.indent) p)) ^
   1.120 +            "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
   1.121 +          #> space_implode "\\par\\smallskip%\n"
   1.122 +          #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   1.123 +        else
   1.124 +          map (fn (p, name) =>
   1.125 +            Output.output (Pretty.str_of p) ^
   1.126 +            "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
   1.127 +          #> space_implode "\\par\\smallskip%\n"
   1.128 +          #> enclose "\\isa{" "}"));
   1.129  
   1.130  
   1.131 -(* theory files *)
   1.132 +(* theory file *)
   1.133  
   1.134 -val _ = ThyOutput.add_commands
   1.135 - [("thy_file", ThyOutput.args (Scan.lift Args.name) (ThyOutput.output (fn _ => fn name =>
   1.136 -      (ThyLoad.check_thy Path.current name; Pretty.str name))))];
   1.137 +val _ = ThyOutput.antiquotation "thy_file" (Scan.lift Args.name)
   1.138 +  (fn _ => fn name => (ThyLoad.check_thy Path.current name; ThyOutput.output [Pretty.str name]));
   1.139  
   1.140  
   1.141 -(* Isabelle entities (with index) *)
   1.142 +(* Isabelle/Isar entities (with index) *)
   1.143  
   1.144  local
   1.145  
   1.146 @@ -147,56 +130,56 @@
   1.147  
   1.148  val arg = enclose "{" "}" o clean_string;
   1.149  
   1.150 -fun output_entity check markup index kind ctxt (logic, name) =
   1.151 -  let
   1.152 -    val hyper_name = "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
   1.153 -    val hyper =
   1.154 -      enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
   1.155 -      index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
   1.156 -    val idx =
   1.157 -      (case index of
   1.158 -        NONE => ""
   1.159 -      | SOME is_def =>
   1.160 -          "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
   1.161 -  in
   1.162 -    if check ctxt name then
   1.163 -      idx ^
   1.164 -      (Output.output name
   1.165 -        |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
   1.166 -        |> (if ! ThyOutput.quotes then quote else I)
   1.167 -        |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   1.168 -            else hyper o enclose "\\mbox{\\isa{" "}}"))
   1.169 -    else error ("Bad " ^ kind ^ " " ^ quote name)
   1.170 -  end;
   1.171 -
   1.172 -fun entity check markup index kind =
   1.173 -  ThyOutput.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
   1.174 -    (K (output_entity check markup index kind));
   1.175 +fun entity check markup kind index =
   1.176 +  ThyOutput.antiquotation
   1.177 +    (case index of NONE => kind | SOME true => kind ^ "_def" | SOME false => kind ^ "_ref")
   1.178 +    (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
   1.179 +    (fn {context = ctxt, ...} => fn (logic, name) =>
   1.180 +      let
   1.181 +        val hyper_name =
   1.182 +          "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
   1.183 +        val hyper =
   1.184 +          enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
   1.185 +          index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
   1.186 +        val idx =
   1.187 +          (case index of
   1.188 +            NONE => ""
   1.189 +          | SOME is_def =>
   1.190 +              "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
   1.191 +      in
   1.192 +        if check ctxt name then
   1.193 +          idx ^
   1.194 +          (Output.output name
   1.195 +            |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
   1.196 +            |> (if ! ThyOutput.quotes then quote else I)
   1.197 +            |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   1.198 +                else hyper o enclose "\\mbox{\\isa{" "}}"))
   1.199 +        else error ("Bad " ^ kind ^ " " ^ quote name)
   1.200 +      end);
   1.201  
   1.202  fun entity_antiqs check markup kind =
   1.203 - [(kind, entity check markup NONE kind),
   1.204 -  (kind ^ "_def", entity check markup (SOME true) kind),
   1.205 -  (kind ^ "_ref", entity check markup (SOME false) kind)];
   1.206 + [(entity check markup kind NONE),
   1.207 +  (entity check markup kind (SOME true)),
   1.208 +  (entity check markup kind (SOME false))];
   1.209  
   1.210  in
   1.211  
   1.212 -val _ = ThyOutput.add_commands
   1.213 - (entity_antiqs no_check "" "syntax" @
   1.214 -  entity_antiqs (K (is_some o OuterKeyword.command_keyword)) "isacommand" "command" @
   1.215 -  entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "keyword" @
   1.216 -  entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "element" @
   1.217 -  entity_antiqs (thy_check Method.intern Method.defined) "" "method" @
   1.218 -  entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute" @
   1.219 -  entity_antiqs no_check "" "fact" @
   1.220 -  entity_antiqs no_check "" "variable" @
   1.221 -  entity_antiqs no_check "" "case" @
   1.222 -  entity_antiqs (K ThyOutput.defined_command) "" "antiquotation" @
   1.223 -  entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @
   1.224 -  entity_antiqs no_check "" "inference" @
   1.225 -  entity_antiqs no_check "isatt" "executable" @
   1.226 -  entity_antiqs (K check_tool) "isatt" "tool" @
   1.227 -  entity_antiqs (K (File.exists o Path.explode)) "isatt" "file" @
   1.228 -  entity_antiqs (K ThyInfo.known_thy) "" "theory");
   1.229 +val _ = entity_antiqs no_check "" "syntax";
   1.230 +val _ = entity_antiqs (K (is_some o OuterKeyword.command_keyword)) "isacommand" "command";
   1.231 +val _ = entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "keyword";
   1.232 +val _ = entity_antiqs (K OuterKeyword.is_keyword) "isakeyword" "element";
   1.233 +val _ = entity_antiqs (thy_check Method.intern Method.defined) "" "method";
   1.234 +val _ = entity_antiqs (thy_check Attrib.intern Attrib.defined) "" "attribute";
   1.235 +val _ = entity_antiqs no_check "" "fact";
   1.236 +val _ = entity_antiqs no_check "" "variable";
   1.237 +val _ = entity_antiqs no_check "" "case";
   1.238 +val _ = entity_antiqs (K ThyOutput.defined_command) "" "antiquotation";
   1.239 +val _ = entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting";
   1.240 +val _ = entity_antiqs no_check "" "inference";
   1.241 +val _ = entity_antiqs no_check "isatt" "executable";
   1.242 +val _ = entity_antiqs (K check_tool) "isatt" "tool";
   1.243 +val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
   1.244 +val _ = entity_antiqs (K ThyInfo.known_thy) "" "theory";
   1.245  
   1.246  end;
   1.247  
     2.1 --- a/doc-src/more_antiquote.ML	Mon Mar 09 20:29:45 2009 +0100
     2.2 +++ b/doc-src/more_antiquote.ML	Mon Mar 09 20:34:11 2009 +0100
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      Doc/more_antiquote.ML
     2.5 +(*  Title:      doc-src/more_antiquote.ML
     2.6      Author:     Florian Haftmann, TU Muenchen
     2.7  
     2.8  More antiquotations.
     2.9 @@ -12,15 +12,13 @@
    2.10  structure More_Antiquote : MORE_ANTIQUOTE =
    2.11  struct
    2.12  
    2.13 -structure O = ThyOutput;
    2.14 -
    2.15  (* printing typewriter lines *)
    2.16  
    2.17  fun typewriter s =
    2.18    let
    2.19      val parse = Scan.repeat
    2.20        (Scan.this_string "\n" |-- Scan.succeed "\\\\\n\\hspace*{0pt}"
    2.21 -        || (Scan.this_string " " 
    2.22 +        || (Scan.this_string " "
    2.23            || Scan.this_string "."
    2.24            || Scan.this_string ","
    2.25            || Scan.this_string ":"
    2.26 @@ -66,9 +64,8 @@
    2.27  
    2.28  in
    2.29  
    2.30 -val _ = O.add_commands
    2.31 -  [("class", ThyOutput.args (Scan.lift Args.name) (K pr_class)),
    2.32 -    ("type", ThyOutput.args (Scan.lift Args.name) (K pr_type))]
    2.33 +val _ = ThyOutput.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
    2.34 +val _ = ThyOutput.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
    2.35  
    2.36  end;
    2.37  
    2.38 @@ -96,12 +93,12 @@
    2.39      val thms = Code_Wellsorted.eqns funcgr const
    2.40        |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    2.41        |> map (holize o no_vars ctxt o AxClass.overload thy);
    2.42 -  in ThyOutput.output_list pretty_thm src ctxt thms end;
    2.43 +  in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;
    2.44  
    2.45  in
    2.46  
    2.47 -val _ = O.add_commands
    2.48 -  [("code_thms", ThyOutput.args Args.term pretty_code_thm)];
    2.49 +val _ = ThyOutput.antiquotation "code_thms" Args.term
    2.50 +  (fn {source, context, ...} => pretty_code_thm source context);
    2.51  
    2.52  end;
    2.53  
    2.54 @@ -120,21 +117,20 @@
    2.55      >> (fn classes => fn thy => fn naming => map_filter (Code_Thingol.lookup_class naming o Sign.intern_class thy) classes);
    2.56    val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name))
    2.57      >> (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);
    2.58 -  val parse_names = parse_consts || parse_types || parse_classes || parse_instances; 
    2.59 -
    2.60 -  fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) =
    2.61 -    Code_Target.code_of (ProofContext.theory_of ctxt)
    2.62 -      target "Example" (mk_cs (ProofContext.theory_of ctxt))
    2.63 -        (fn naming => maps (fn f => f (ProofContext.theory_of ctxt) naming) mk_stmtss)
    2.64 -    |> typewriter;
    2.65 +  val parse_names = parse_consts || parse_types || parse_classes || parse_instances;
    2.66  
    2.67  in
    2.68  
    2.69 -val _ = O.add_commands
    2.70 -  [("code_stmts", O.args
    2.71 -      (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
    2.72 -        code_stmts)]
    2.73 -
    2.74 -end
    2.75 +val _ = ThyOutput.antiquotation "code_stmts"
    2.76 +  (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
    2.77 +  (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
    2.78 +    let val thy = ProofContext.theory_of ctxt in
    2.79 +      Code_Target.code_of thy
    2.80 +        target "Example" (mk_cs thy)
    2.81 +        (fn naming => maps (fn f => f thy naming) mk_stmtss)
    2.82 +      |> typewriter
    2.83 +    end);
    2.84  
    2.85  end;
    2.86 +
    2.87 +end;
     3.1 --- a/src/Pure/Thy/thy_output.ML	Mon Mar 09 20:29:45 2009 +0100
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Mar 09 20:34:11 2009 +0100
     3.3 @@ -590,8 +590,9 @@
     3.4  
     3.5  val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
     3.6  val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
     3.7 -val _ = ml_text "ML_struct"
     3.8 -  (fn txt => "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;");
     3.9 +val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;");
    3.10 +val _ = ml_text "ML_functor" (K "");  (*no check!*)
    3.11 +val _ = ml_text "ML_text" (K "");
    3.12  
    3.13  end;
    3.14