1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Local_Method
8imports Main
9keywords "supply_local_method" :: prf_script % "proof"
10begin
11
12text \<open>See documentation in @{path Local_Method_Tests.thy}.\<close>
13
14ML \<open>
15  structure MethodData = Proof_Data(
16    type T = Method.method Symtab.table
17    val init = K Symtab.empty);
18\<close>
19
20method_setup local_method = \<open>
21  Scan.lift Parse.liberal_name >>
22  (fn name => fn _ => fn facts => fn (ctxt, st) =>
23    case (ctxt |> MethodData.get |> Symtab.lookup) name of
24        SOME method => method facts (ctxt, st)
25      | NONE => Seq.succeed (Seq.Error (K ("Couldn't find method text named " ^ quote name))))
26\<close>
27
28ML \<open>
29local
30
31val parse_name_text_ranges =
32  Scan.repeat1 (Parse.liberal_name --| Parse.!!! @{keyword "="} -- Method.parse)
33
34fun supply_method_cmd name_text_ranges ctxt =
35  let
36    fun add_method ((name, (text, range)), ctxt) =
37      let
38        val _ = Method.report (text, range)
39        val method = Method.evaluate text ctxt
40      in
41        MethodData.map (Symtab.update (name, method)) ctxt
42      end
43  in
44    List.foldr add_method ctxt name_text_ranges
45  end
46
47val _ =
48  Outer_Syntax.command @{command_keyword\<open>supply_local_method\<close>}
49    "Add a local method alias to the current proof context"
50    (parse_name_text_ranges >> (Toplevel.proof o Proof.map_context o supply_method_cmd))
51
52in end
53\<close>
54
55end