| author | Christian Urban <urbanc@in.tum.de> |
| Wed, 14 Jan 2009 23:44:14 +0000 | |
| changeset 72 | 7b8c4fe235aa |
| parent 57 | 065f472c09ab |
| child 73 | bcbcf5c839ae |
| permissions | -rw-r--r-- |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
(* Auxiliary antiquotations for the Cookbook. *) |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
structure AntiquoteSetup: sig end = |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
struct |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
|
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
6 |
(* rebuilding the output_list function from ThyOutput in order to *) |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
7 |
(* enable the option [gray] *) |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
8 |
|
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
9 |
val gray = ref false; |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
10 |
|
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
11 |
fun boolean "" = true |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
12 |
| boolean "true" = true |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
13 |
| boolean "false" = false |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
14 |
| boolean s = error ("Bad boolean value: " ^ quote s);
|
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
15 |
|
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
16 |
fun output_list pretty src ctxt xs = |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
17 |
map (pretty ctxt) xs (*always pretty in order to exhibit errors!*) |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
18 |
|> (if ! ThyOutput.source then K [ThyOutput.pretty_text (ThyOutput.str_of_source src)] else I) |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
19 |
|> (if ! ThyOutput.quotes then map Pretty.quote else I) |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
20 |
|> (if ! ThyOutput.display then |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
21 |
map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent)) |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
22 |
#> space_implode "\\isasep\\isanewline%\n" |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
23 |
#> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I)
|
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
24 |
#> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
|
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
25 |
else |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
26 |
(*map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))*) |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
27 |
map (Output.output o Pretty.str_of) |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
28 |
#> space_implode "\\isasep\\isanewline%\n" |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
29 |
#> enclose "\\isa{" "}");
|
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
30 |
|
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
31 |
val _ = ThyOutput.add_options |
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
32 |
[("gray", Library.setmp gray o boolean)]
|
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
33 |
|
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
34 |
|
|
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
35 |
(* main body *) |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
fun ml_val_open (ys, xs) txt = |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
let fun ml_val_open_aux ys txt = |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
"fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
in |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
(case xs of |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
[] => ml_val_open_aux ys txt |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
| _ => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end"))
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |
end; |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
fun ml_val txt = ml_val_open ([],[]) txt; |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
fun ml_pat (rhs, pat) = |
|
51
c346c156a7cd
completes the recipie on antiquotations
Christian Urban <urbanc@in.tum.de>
parents:
49
diff
changeset
|
48 |
let |
|
c346c156a7cd
completes the recipie on antiquotations
Christian Urban <urbanc@in.tum.de>
parents:
49
diff
changeset
|
49 |
val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat)) |
|
c346c156a7cd
completes the recipie on antiquotations
Christian Urban <urbanc@in.tum.de>
parents:
49
diff
changeset
|
50 |
in "val " ^ pat' ^ " = " ^ rhs end; |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
51 |
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
52 |
fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
54 |
|
|
57
065f472c09ab
Repaired output of marginal comments in ML antiquotation.
berghofe
parents:
54
diff
changeset
|
55 |
val transform_cmts_str = |
|
065f472c09ab
Repaired output of marginal comments in ML antiquotation.
berghofe
parents:
54
diff
changeset
|
56 |
Source.of_string #> ML_Lex.source #> Source.exhaust #> |
|
065f472c09ab
Repaired output of marginal comments in ML antiquotation.
berghofe
parents:
54
diff
changeset
|
57 |
Chunks.transform_cmts #> implode; |
|
065f472c09ab
Repaired output of marginal comments in ML antiquotation.
berghofe
parents:
54
diff
changeset
|
58 |
|
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
59 |
fun output_ml ml src ctxt ((txt,ovars),pos) = |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
(ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt); |
|
57
065f472c09ab
Repaired output of marginal comments in ML antiquotation.
berghofe
parents:
54
diff
changeset
|
61 |
txt |> transform_cmts_str |> space_explode "\n" |> |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
62 |
output_list (fn _ => fn s => Pretty.str s) src ctxt) |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
|
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
64 |
fun output_ml_aux ml src ctxt (txt,pos) = |
|
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
65 |
output_ml (K ml) src ctxt ((txt,()),pos) |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
fun add_response_indicator txt = |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
map (fn s => "> " ^ s) (space_explode "\n" txt) |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
(ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); |
|
51
c346c156a7cd
completes the recipie on antiquotations
Christian Urban <urbanc@in.tum.de>
parents:
49
diff
changeset
|
72 |
let |
|
c346c156a7cd
completes the recipie on antiquotations
Christian Urban <urbanc@in.tum.de>
parents:
49
diff
changeset
|
73 |
val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
74 |
in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
75 |
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
(ML_Context.eval_in (SOME ctxt) false pos (ml lhs); |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
79 |
in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
80 |
|
|
54
1783211b3494
tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents:
53
diff
changeset
|
81 |
fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = |
|
1783211b3494
tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents:
53
diff
changeset
|
82 |
let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents:
57
diff
changeset
|
83 |
in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end |
|
54
1783211b3494
tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents:
53
diff
changeset
|
84 |
|
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
85 |
fun check_file_exists ctxt txt = |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
86 |
if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then ()
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
87 |
else error ("Source file " ^ quote txt ^ " does not exist.")
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
88 |
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
89 |
val _ = ThyOutput.add_commands |
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
90 |
[("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name --
|
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
91 |
(Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
92 |
Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))) |
|
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
93 |
(output_ml ml_val_open)), |
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
94 |
("ML_file", ThyOutput.args (Scan.lift Args.name)
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
95 |
(ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))), |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
96 |
("ML_text", ThyOutput.args (Scan.lift Args.name)
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
97 |
(ThyOutput.output (fn _ => fn s => Pretty.str s))), |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
98 |
("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name)))
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
99 |
(output_ml_response ml_pat)), |
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
100 |
("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name)))
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
101 |
(output_ml_response_fake ml_val)), |
|
54
1783211b3494
tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents:
53
diff
changeset
|
102 |
("ML_response_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name)))
|
|
1783211b3494
tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents:
53
diff
changeset
|
103 |
(output_ml_response_fake_both ml_val)), |
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
104 |
("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)),
|
|
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents:
51
diff
changeset
|
105 |
("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type))];
|
|
45
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
106 |
|
|
78aeca00bb54
deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
107 |
end; |