# HG changeset patch # User wenzelm # Date 1695651463 -7200 # Node ID c7b2697094ac8de45320a1a3b416c0b65056814b # Parent e10ef4f9c84847ac381ee7fe6775257bbd27b69a more general ML_Antiquotation.special_form; more general "try" forms: support 'finally' or 'catch'; diff -r e10ef4f9c848 -r c7b2697094ac src/Pure/Concurrent/isabelle_thread.ML --- a/src/Pure/Concurrent/isabelle_thread.ML Sun Sep 24 15:55:42 2023 +0200 +++ b/src/Pure/Concurrent/isabelle_thread.ML Mon Sep 25 16:17:43 2023 +0200 @@ -24,6 +24,8 @@ val interrupt_exn: 'a Exn.result val interrupt_self: unit -> 'a val interrupt_other: T -> unit + val try_catch: (unit -> 'a) -> (exn -> 'a) -> 'a + val try_finally: (unit -> 'a) -> (unit -> unit) -> 'a val try: (unit -> 'a) -> 'a option val can: (unit -> 'a) -> bool end; @@ -117,6 +119,12 @@ fun interrupt_other t = Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => (); +fun try_catch e f = + e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else f exn; + +fun try_finally e f = + Exn.release (Exn.capture e () before f ()); + fun try e = Basics.try e (); fun can e = Basics.can e (); diff -r e10ef4f9c848 -r c7b2697094ac src/Pure/ML/ml_antiquotation.ML --- a/src/Pure/ML/ml_antiquotation.ML Sun Sep 24 15:55:42 2023 +0200 +++ b/src/Pure/ML/ml_antiquotation.ML Mon Sep 25 16:17:43 2023 +0200 @@ -18,7 +18,9 @@ val inline_embedded: binding -> string context_parser -> theory -> theory val value: binding -> string context_parser -> theory -> theory val value_embedded: binding -> string context_parser -> theory -> theory - val special_form: binding -> string -> theory -> theory + val special_form: binding -> + (Proof.context -> Input.source -> string * ML_Lex.token Antiquote.antiquote list list) -> + theory -> theory val conditional: binding -> (Proof.context -> bool) -> theory -> theory end; @@ -67,23 +69,31 @@ (* ML macros *) -fun special_form binding operator = +fun special_form binding parse = ML_Context.add_antiquotation binding true (fn _ => fn src => fn ctxt => let - val s = Token.read ctxt Parse.embedded_input src; + val input = Token.read ctxt Parse.embedded_input src; val tokenize = ML_Lex.tokenize_no_range; - val tokenize_range = ML_Lex.tokenize_range (Input.range_of s); + val tokenize_range = ML_Lex.tokenize_range (Input.range_of input); + val eq = tokenize " = "; - val (decl, ctxt') = ML_Context.read_antiquotes s ctxt; + val (operator, sections) = parse ctxt input; + val (decls, ctxt') = ML_Context.expand_antiquotes_list sections ctxt; fun decl' ctxt'' = let - val (ml_env, ml_body) = decl ctxt''; + val (sections_env, sections_body) = split_list (decls ctxt''); + val sections_bind = + sections_body |> map_index (fn (i, body) => + let + val name = tokenize ("expr" ^ (if i = 0 then "" else string_of_int i)); + val bind = if i = 0 then tokenize "val " else tokenize "and "; + in (bind @ name @ eq @ body, name) end); val ml_body' = - tokenize "let val expr = (fn () => " @ ml_body @ tokenize ");" @ - tokenize " val " @ tokenize_range "result" @ - tokenize (" = " ^ operator ^ " expr; in result end"); - in (ml_env, ml_body') end; + tokenize "let " @ maps #1 sections_bind @ + tokenize " val " @ tokenize_range "result" @ eq @ + tokenize operator @ maps #2 sections_bind @ tokenize " in result end"; + in (flat sections_env, ml_body') end; in (decl', ctxt') end); fun conditional binding check = diff -r e10ef4f9c848 -r c7b2697094ac src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Sun Sep 24 15:55:42 2023 +0200 +++ b/src/Pure/ML/ml_antiquotations.ML Mon Sep 25 16:17:43 2023 +0200 @@ -340,12 +340,68 @@ in end; -(* special forms for option type *) +(* exception handling *) + +local + +val tokenize = ML_Lex.tokenize_no_range; +val tokenize_range = ML_Lex.tokenize_range o Input.range_of; +val tokenize_text = map Antiquote.Text o ML_Lex.tokenize_no_range; + +val bg_expr = tokenize_text "(fn () =>"; +val en_expr = tokenize_text ")"; +fun make_expr a = bg_expr @ a @ en_expr; + +val bg_handler = tokenize_text "(fn"; +val en_handler = tokenize_text "| exn => Exn.reraise exn)"; +fun make_handler a = bg_handler @ a @ en_handler; + +fun report_special tok = (ML_Lex.pos_of tok, Markup.keyword3); + +fun print_special tok = + let val (pos, markup) = report_special tok + in Markup.markup markup (ML_Lex.content_of tok) ^ Position.here pos end; + +val is_catch = ML_Lex.is_ident_with (fn x => x = "catch"); +val is_finally = ML_Lex.is_ident_with (fn x => x = "finally"); +fun is_special t = is_catch t orelse is_finally t; +val is_special_text = fn Antiquote.Text t => is_special t | _ => false; + +fun parse_try ctxt input = + let + val ants = ML_Lex.read_source input; + val specials = ants + |> map_filter (fn Antiquote.Text t => if is_special t then SOME t else NONE | _ => NONE); + val _ = Context_Position.reports ctxt (map report_special specials); + in + (case specials of + [] => ("Isabelle_Thread.try", [make_expr ants]) + | [s] => + let val (a, b) = ants |> chop_prefix (not o is_special_text) ||> tl in + if is_finally s + then ("Isabelle_Thread.try_finally", [make_expr a, make_expr b]) + else ("Isabelle_Thread.try_catch", [make_expr a, make_handler b]) + end + | _ => error ("Too many special keywords: " ^ commas (map print_special specials))) + end; + +fun parse_can (_: Proof.context) input = + ("Isabelle_Thread.can", [make_expr (ML_Lex.read_source input)]); + +in val _ = Theory.setup - (ML_Antiquotation.special_form \<^binding>\try\ "Isabelle_Thread.try" #> - ML_Antiquotation.special_form \<^binding>\can\ "Isabelle_Thread.can" #> - ML_Context.add_antiquotation \<^binding>\if_none\ true + (ML_Antiquotation.special_form \<^binding>\try\ parse_try #> + ML_Antiquotation.special_form \<^binding>\can\ parse_can); + +end; + + + +(* special form for option type *) + +val _ = Theory.setup + (ML_Context.add_antiquotation \<^binding>\if_none\ true (fn _ => fn src => fn ctxt => let val s = Token.read ctxt Parse.embedded_input src; diff -r e10ef4f9c848 -r c7b2697094ac src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Sun Sep 24 15:55:42 2023 +0200 +++ b/src/Pure/ML/ml_lex.ML Mon Sep 25 16:17:43 2023 +0200 @@ -12,6 +12,7 @@ Space | Comment of Comment.kind option | Error of string | EOF eqtype token val stopper: token Scan.stopper + val is_ident_with: (string -> bool) -> token -> bool val is_regular: token -> bool val is_improper: token -> bool val is_comment: token -> bool @@ -110,6 +111,9 @@ fun is_delimiter (Token (_, (Keyword, x))) = not (Symbol.is_ascii_identifier x) | is_delimiter _ = false; +fun is_ident_with pred (Token (_, (Ident, x))) = pred x + | is_ident_with _ _ = false; + fun is_regular (Token (_, (Error _, _))) = false | is_regular (Token (_, (EOF, _))) = false | is_regular _ = true;