49 |
49 |
50 (* ML text *) |
50 (* ML text *) |
51 |
51 |
52 local |
52 local |
53 |
53 |
54 fun ml_val (txt1, "") = "fn _ => (" ^ txt1 ^ ");" |
54 val ml_toks = ML_Lex.read Position.none; |
55 | ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ " : " ^ txt2 ^ ");"; |
55 |
56 |
56 fun ml_val (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks ");" |
57 fun ml_op (txt1, "") = "fn _ => (op " ^ txt1 ^ ");" |
57 | ml_val (toks1, toks2) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");"; |
58 | ml_op (txt1, txt2) = "fn _ => (op " ^ txt1 ^ " : " ^ txt2 ^ ");"; |
58 |
59 |
59 fun ml_op (toks1, []) = ml_toks "fn _ => (op " @ toks1 @ ml_toks ");" |
60 fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;" |
60 | ml_op (toks1, toks2) = ml_toks "fn _ => (op " @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");"; |
61 | ml_type (txt1, txt2) = "val _ = [NONE : (" ^ txt1 ^ ") option, NONE : (" ^ txt2 ^ ") option];"; |
61 |
62 |
62 fun ml_type (toks1, []) = ml_toks "val _ = NONE : (" @ toks1 @ ml_toks ") option;" |
63 fun ml_exn (txt1, "") = "fn _ => (" ^ txt1 ^ " : exn);" |
63 | ml_type (toks1, toks2) = |
64 | ml_exn (txt1, txt2) = "fn _ => (" ^ txt1 ^ " : " ^ txt2 ^ " -> exn);"; |
64 ml_toks "val _ = [NONE : (" @ toks1 @ ml_toks ") option, NONE : (" @ |
65 |
65 toks2 @ ml_toks ") option];"; |
66 fun ml_structure (txt, _) = "functor XXX() = struct structure XX = " ^ txt ^ " end;"; |
66 |
67 |
67 fun ml_exn (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);" |
68 fun ml_functor (txt, _) = "ML_Env.check_functor " ^ ML_Syntax.print_string txt; |
68 | ml_exn (toks1, toks2) = |
|
69 ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks " -> exn);"; |
|
70 |
|
71 fun ml_structure (toks, _) = |
|
72 ml_toks "functor XXX() = struct structure XX = " @ toks @ ml_toks " end;"; |
|
73 |
|
74 fun ml_functor (Antiquote.Text tok :: _, _) = |
|
75 ml_toks "ML_Env.check_functor " @ ml_toks (ML_Syntax.print_string (ML_Lex.content_of tok)) |
|
76 | ml_functor _ = raise Fail "Bad ML functor specification"; |
69 |
77 |
70 val is_name = ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.LongIdent); |
78 val is_name = ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.LongIdent); |
71 |
79 |
72 fun ml_name txt = |
80 fun ml_name txt = |
73 (case filter is_name (ML_Lex.tokenize txt) of |
81 (case filter is_name (ML_Lex.tokenize txt) of |
74 toks as [_] => ML_Lex.flatten toks |
82 toks as [_] => ML_Lex.flatten toks |
75 | _ => error ("Single ML name expected in input: " ^ quote txt)); |
83 | _ => error ("Single ML name expected in input: " ^ quote txt)); |
76 |
84 |
|
85 fun prep_ml source = |
|
86 (#1 (Symbol_Pos.source_content source), ML_Lex.read_source source); |
|
87 |
77 fun index_ml name kind ml = Thy_Output.antiquotation name |
88 fun index_ml name kind ml = Thy_Output.antiquotation name |
78 (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) |
89 (Scan.lift (Args.name_source_position -- Scan.option (Args.colon |-- Args.name_source_position))) |
79 (fn {context = ctxt, ...} => fn (txt1, txt2) => |
90 (fn {context = ctxt, ...} => fn (source1, opt_source2) => |
80 let |
91 let |
|
92 val (txt1, toks1) = prep_ml source1; |
|
93 val (txt2, toks2) = |
|
94 (case opt_source2 of |
|
95 SOME source => prep_ml source |
|
96 | NONE => ("", [])); |
|
97 |
81 val txt = |
98 val txt = |
82 if txt2 = "" then txt1 |
99 if txt2 = "" then txt1 |
83 else if kind = "type" then txt1 ^ " = " ^ txt2 |
100 else if kind = "type" then txt1 ^ " = " ^ txt2 |
84 else if kind = "exception" then txt1 ^ " of " ^ txt2 |
101 else if kind = "exception" then txt1 ^ " of " ^ txt2 |
85 else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1)) |
102 else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1)) |
86 then txt1 ^ ": " ^ txt2 |
103 then txt1 ^ ": " ^ txt2 |
87 else txt1 ^ " : " ^ txt2; |
104 else txt1 ^ " : " ^ txt2; |
88 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
105 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
89 val _ = (* ML_Lex.read (!?) *) |
106 |
90 ML_Context.eval_source_in (SOME ctxt) false |
107 val _ = ML_Context.eval_in (SOME ctxt) false (#pos source1) (ml (toks1, toks2)); |
91 {delimited = false, text = ml (txt1, txt2), pos = Position.none}; |
|
92 val kind' = if kind = "" then "ML" else "ML " ^ kind; |
108 val kind' = if kind = "" then "ML" else "ML " ^ kind; |
93 in |
109 in |
94 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
110 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
95 (txt' |
111 (txt' |
96 |> (if Config.get ctxt Thy_Output.quotes then quote else I) |
112 |> (if Config.get ctxt Thy_Output.quotes then quote else I) |
97 |> (if Config.get ctxt Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
113 |> (if Config.get ctxt Thy_Output.display |
|
114 then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
98 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
115 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
99 end); |
116 end); |
100 |
117 |
101 in |
118 in |
102 |
119 |
103 val index_ml_setup = |
120 val index_ml_setup = |
104 index_ml @{binding index_ML} "" ml_val #> |
121 index_ml @{binding index_ML} "" ml_val #> |
105 index_ml @{binding index_ML_op} "infix" ml_op #> |
122 index_ml @{binding index_ML_op} "infix" ml_op #> |
106 index_ml @{binding index_ML_type} "type" ml_type #> |
123 index_ml @{binding index_ML_type} "type" ml_type #> |
107 index_ml @{binding index_ML_exn} "exception" ml_exn #> |
124 index_ml @{binding index_ML_exn} "exception" ml_exn #> |
108 index_ml @{binding index_ML_structure} "structure" ml_structure #> |
125 index_ml @{binding index_ML_struct} "structure" ml_structure #> |
109 index_ml @{binding index_ML_functor} "functor" ml_functor; |
126 index_ml @{binding index_ML_functor} "functor" ml_functor; |
110 |
127 |
111 end; |
128 end; |
112 |
129 |
113 |
130 |