325 fun test_functor (Antiquote.Text tok :: _, _) = |
325 fun test_functor (Antiquote.Text tok :: _, _) = |
326 ML_Lex.read "ML_Env.check_functor " @ |
326 ML_Lex.read "ML_Env.check_functor " @ |
327 ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok)) |
327 ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok)) |
328 | test_functor _ = raise Fail "Bad ML functor specification"; |
328 | test_functor _ = raise Fail "Bad ML functor specification"; |
329 |
329 |
330 val is_name = |
|
331 ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident); |
|
332 |
|
333 fun is_ml_identifier ants = |
|
334 forall Antiquote.is_text ants andalso |
|
335 (case filter is_name (map (Antiquote.the_text "") ants) of |
|
336 toks as [_] => Symbol_Pos.is_identifier (Long_Name.base_name (ML_Lex.flatten toks)) |
|
337 | _ => false); |
|
338 |
|
339 val parse_ml0 = Args.text_input >> rpair Input.empty; |
330 val parse_ml0 = Args.text_input >> rpair Input.empty; |
340 val parse_ml = Args.text_input -- Scan.optional (Args.colon |-- Args.text_input) Input.empty; |
331 val parse_ml = Args.text_input -- Scan.optional (Args.colon |-- Args.text_input) Input.empty; |
341 val parse_type = Args.text_input -- Scan.optional (Args.$$$ "=" |-- Args.text_input) Input.empty; |
332 val parse_type = Args.text_input -- Scan.optional (Args.$$$ "=" |-- Args.text_input) Input.empty; |
342 val parse_exn = Args.text_input -- Scan.optional (Args.$$$ "of" |-- Args.text_input) Input.empty; |
333 val parse_exn = Args.text_input -- Scan.optional (Args.$$$ "of" |-- Args.text_input) Input.empty; |
343 |
334 |
|
335 fun eval ctxt pos ml = |
|
336 ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos ml |
|
337 handle ERROR msg => error (msg ^ Position.here pos); |
|
338 |
|
339 fun make_text sep sources = |
|
340 let |
|
341 val (txt1, txt2) = apply2 (#1 o Input.source_content) sources; |
|
342 val is_ident = |
|
343 (case try List.last (Symbol.explode txt1) of |
|
344 NONE => false |
|
345 | SOME s => Symbol.is_ascii_letdig s); |
|
346 val txt = |
|
347 if txt2 = "" then txt1 |
|
348 else if sep = ":" andalso is_ident then txt1 ^ ": " ^ txt2 |
|
349 else txt1 ^ " " ^ sep ^ " " ^ txt2 |
|
350 in (txt, txt1) end; |
|
351 |
344 fun antiquotation_ml parse test kind show_kind binding index = |
352 fun antiquotation_ml parse test kind show_kind binding index = |
345 Document_Output.antiquotation_raw binding (Scan.lift parse) |
353 Document_Output.antiquotation_raw binding (Scan.lift parse) |
346 (fn ctxt => fn (source1, source2) => |
354 (fn ctxt => fn sources => |
347 let |
355 let |
348 val (ml1, ml2) = apply2 ML_Lex.read_source (source1, source2); |
356 val _ = apply2 ML_Lex.read_source sources |> test |> eval ctxt (Input.pos_of (#1 sources)); |
349 val pos = Input.pos_of source1; |
357 |
350 val _ = |
|
351 ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (test (ml1, ml2)) |
|
352 handle ERROR msg => error (msg ^ Position.here pos); |
|
353 |
|
354 val (txt1, txt2) = apply2 (#1 o Input.source_content) (source1, source2); |
|
355 val sep = if kind = "type" then "=" else if kind = "exception" then "of" else ":"; |
358 val sep = if kind = "type" then "=" else if kind = "exception" then "of" else ":"; |
356 val txt = |
359 val (txt, idx) = make_text sep sources; |
357 if txt2 = "" then txt1 |
|
358 else if sep = ":" andalso is_ml_identifier ml1 then txt1 ^ ": " ^ txt2 |
|
359 else txt1 ^ " " ^ sep ^ " " ^ txt2; |
|
360 |
360 |
361 val main_text = |
361 val main_text = |
362 Document_Output.verbatim ctxt |
362 Document_Output.verbatim ctxt |
363 (if kind = "" orelse not show_kind then txt else kind ^ " " ^ txt); |
363 (if kind = "" orelse not show_kind then txt else kind ^ " " ^ txt); |
364 |
364 |
365 val index_text = |
365 val index_text = |
366 index |> Option.map (fn def => |
366 index |> Option.map (fn def => |
367 let |
367 let |
368 val ctxt' = Config.put Document_Antiquotation.thy_output_display false ctxt; |
368 val ctxt' = Config.put Document_Antiquotation.thy_output_display false ctxt; |
369 val kind' = if kind = "" then " (ML)" else " (ML " ^ kind ^ ")"; |
369 val kind' = if kind = "" then " (ML)" else " (ML " ^ kind ^ ")"; |
370 val txt' = Latex.block [Document_Output.verbatim ctxt' txt1, Latex.string kind']; |
370 val txt' = Latex.block [Document_Output.verbatim ctxt' idx, Latex.string kind']; |
371 val like = Document_Antiquotation.approx_content ctxt' txt1; |
371 val like = Document_Antiquotation.approx_content ctxt' idx; |
372 in Latex.index_entry {items = [{text = txt', like = like}], def = def} end); |
372 in Latex.index_entry {items = [{text = txt', like = like}], def = def} end); |
373 in Latex.block (the_list index_text @ [main_text]) end); |
373 in Latex.block (the_list index_text @ [main_text]) end); |
374 |
374 |
375 fun antiquotation_ml0 test kind = |
375 fun antiquotation_ml0 test kind = |
376 antiquotation_ml parse_ml0 test kind false; |
376 antiquotation_ml parse_ml0 test kind false; |