Mercurial Mercurial > hg > isabelle-cookbook / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ProgTutorial/antiquote_setup.ML
changeset 449 f952f2679a11
parent 438 d9a223c023f6
child 470 817ecad4cf72
equal deleted inserted replaced
448:957f69b9b7df 449:f952f2679a11 
    36   ML_Context.eval_text_in (SOME ctxt) false Position.none exp
 
    36   ML_Context.eval_text_in (SOME ctxt) false Position.none exp
 
    37 
    37 
    38 (* checks and prints a possibly open expressions, no index *)
 
    38 (* checks and prints a possibly open expressions, no index *)
 
    39 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) =
 
    39 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) =
 
    40   (eval_fn ctxt (ml_val vs stru txt); 
    40   (eval_fn ctxt (ml_val vs stru txt); 
    41    output (split_lines txt))
 
    41    output ctxt (split_lines txt))
 
    42 
    42 
    43 val parser_ml = Scan.lift (Args.name --
 
    43 val parser_ml = Scan.lift (Args.name --
 
    44   (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] --
 
    44   (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] --
 
    45    Scan.option (Args.$$$ "in"  |-- Parse.!!! Args.name))) 
    45    Scan.option (Args.$$$ "in"  |-- Parse.!!! Args.name))) 
    46 
    46 
    47 (* checks and prints a single ML-item and produces an index entry *)
 
    47 (* checks and prints a single ML-item and produces an index entry *)
 
    48 fun output_ml_ind {context = ctxt, ...} (txt, stru) =
 
    48 fun output_ml_ind {context = ctxt, ...} (txt, stru) =
 
    49   (eval_fn ctxt (ml_val [] stru txt); 
    49   (eval_fn ctxt (ml_val [] stru txt); 
    50    case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
 
    50    case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
 
    51      (NONE, bn, "")  => output_indexed {main = Code txt, minor = NoString} (split_lines txt)
 
    51      (NONE, bn, "")  => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt)
 
    52    | (NONE, bn, qn)  => output_indexed {main = Code bn,  minor = Struct qn} (split_lines txt)
 
    52    | (NONE, bn, qn)  => output_indexed ctxt {main = Code bn,  minor = Struct qn} (split_lines txt)
 
    53    | (SOME st, _, _) => output_indexed {main = Code txt, minor = Struct st} (split_lines txt))
 
    53    | (SOME st, _, _) => output_indexed ctxt {main = Code txt, minor = Struct st} (split_lines txt))
 
    54 
    54 
    55 val parser_ml_ind = Scan.lift (Args.name --
 
    55 val parser_ml_ind = Scan.lift (Args.name --
 
    56   Scan.option (Args.$$$ "in"  |-- Parse.!!! Args.name))
 
    56   Scan.option (Args.$$$ "in"  |-- Parse.!!! Args.name))
 
    57 
    57 
    58 (* checks and prints structures *)
 
    58 (* checks and prints structures *)
 
    59 fun gen_output_struct outfn {context = ctxt, ...} txt = 
    59 fun gen_output_struct outfn ctxt txt = 
    60   (eval_fn ctxt (ml_struct txt); 
    60   (eval_fn ctxt (ml_struct txt); 
    61    outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
 
    61    outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
 
    62 
    62 
    63 val output_struct = gen_output_struct (K output)
 
    63 fun output_struct {context = ctxt, ...} = gen_output_struct (K (output ctxt)) ctxt 
    64 val output_struct_ind = gen_output_struct output_indexed
 
    64 fun output_struct_ind {context = ctxt, ...} = gen_output_struct (output_indexed ctxt) ctxt 
    65 
    65 
    66 (* prints functors; no checks *)
 
    66 (* prints functors; no checks *)
 
    67 fun gen_output_funct outfn {context = ctxt, ...} txt = 
    67 fun gen_output_funct outfn txt = 
    68   (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))
 
    68   (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))
 
    69 
    69 
    70 val output_funct = gen_output_funct (K output)
 
    70 fun output_funct {context = ctxt, ...} = gen_output_funct (K (output ctxt)) 
    71 val output_funct_ind = gen_output_funct output_indexed
 
    71 fun output_funct_ind {context = ctxt, ...} = gen_output_funct (output_indexed ctxt)
 
    72 
    72 
    73 (* checks and prints types *)
 
    73 (* checks and prints types *)
 
    74 fun gen_output_type outfn {context = ctxt, ...} txt = 
    74 fun gen_output_type outfn ctxt txt = 
    75   (eval_fn ctxt (ml_type txt); 
    75   (eval_fn ctxt (ml_type txt); 
    76    outfn {main = Code txt, minor = Plain "type"} (split_lines txt))
 
    76    outfn {main = Code txt, minor = Plain "type"} (split_lines txt))
 
    77 
    77 
    78 val output_type = gen_output_type (K output)
 
    78 fun output_type {context = ctxt, ...} = gen_output_type (K (output ctxt)) ctxt
 
    79 val output_type_ind = gen_output_type output_indexed
 
    79 fun output_type_ind {context = ctxt, ...} = gen_output_type (output_indexed ctxt) ctxt 
    80 
    80 
    81 (* checks and expression agains a result pattern *)
 
    81 (* checks and expression agains a result pattern *)
 
    82 fun output_response {context = ctxt, ...} (lhs, pat) = 
    82 fun output_response {context = ctxt, ...} (lhs, pat) = 
    83     (eval_fn ctxt (ml_pat (lhs, pat));
 
    83     (eval_fn ctxt (ml_pat (lhs, pat));
 
    84      write_file_ml_blk lhs (ProofContext.theory_of ctxt);
 
    84      write_file_ml_blk lhs (ProofContext.theory_of ctxt);
 
    85      output ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
    85      output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
    86 
    86 
    87 (* checks the expressions, but does not check it against a result pattern *)
 
    87 (* checks the expressions, but does not check it against a result pattern *)
 
    88 fun output_response_fake {context = ctxt, ...} (lhs, pat) = 
    88 fun output_response_fake {context = ctxt, ...} (lhs, pat) = 
    89     (eval_fn ctxt (ml_val [] NONE lhs);
 
    89     (eval_fn ctxt (ml_val [] NONE lhs);
 
    90      write_file_ml_blk lhs (ProofContext.theory_of ctxt);
 
    90      write_file_ml_blk lhs (ProofContext.theory_of ctxt);
 
    91      output ((split_lines lhs) @ (prefix_lines "> " pat)))
 
    91      output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)))
 
    92 
    92 
    93 (* checks the expressions, but does not check it against a result pattern *)
 
    93 (* checks the expressions, but does not check it against a result pattern *)
 
    94 fun ouput_response_fake_both _ (lhs, pat) = 
    94 fun ouput_response_fake_both {context = ctxt, ...} (lhs, pat) = 
    95     output ((split_lines lhs) @ (prefix_lines "> " pat))
 
    95     output ctxt ((split_lines lhs) @ (prefix_lines "> " pat))
 
    96 
    96 
    97 val single_arg = Scan.lift (Args.name)
 
    97 val single_arg = Scan.lift (Args.name)
 
    98 val two_args   = Scan.lift (Args.name -- Args.name)
 
    98 val two_args   = Scan.lift (Args.name -- Args.name)
 
    99 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with"  |-- Args.name))
 
    99 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with"  |-- Args.name))
 
   100 
   100 
   116 
   116 
   117 fun output_response_eq {context = ctxt, ...} ((lhs, pat), eq) = 
   117 fun output_response_eq {context = ctxt, ...} ((lhs, pat), eq) = 
   118     (case eq of 
   118     (case eq of 
   119        NONE => eval_fn ctxt (ml_pat (lhs, pat))
 
   119        NONE => eval_fn ctxt (ml_pat (lhs, pat))
 
   120      | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e));
 
   120      | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e));
 
   121      output ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
   121      output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
   122 
   122 
   123 val _ = Thy_Output.antiquotation "ML_response_eq" test output_response_eq
 
   123 val _ = Thy_Output.antiquotation "ML_response_eq" test output_response_eq
 
   124 
   124 
   125 (* checks whether a file exists in the Isabelle distribution *)
 
   125 (* checks whether a file exists in the Isabelle distribution *)
 
   126 fun href_link txt =
 
   126 fun href_link txt =
 
   129   val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"    
   129   val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"    
   130 in
 
   130 in
 
   131  implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"]
 
   131  implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"]
 
   132 end 
   132 end 
   133 
   133 
   134 fun check_file_exists _ txt =
 
   134 fun check_file_exists {context = ctxt, ...} txt =
 
   135   (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 
   135   (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 
   136    then output [href_link txt]
 
   136    then output ctxt [href_link txt]
 
   137    else error (implode ["Source file ", quote txt, " does not exist."]))
 
   137    else error (implode ["Source file ", quote txt, " does not exist."]))
 
   138 
   138 
   139 val _ = Thy_Output.antiquotation "ML_file" single_arg check_file_exists
 
   139 val _ = Thy_Output.antiquotation "ML_file" single_arg check_file_exists
 
   140 
   140 
   141 
   141 
   144 fun proof_state state =
 
   144 fun proof_state state =
 
   145     (case try Toplevel.proof_of state of
 
   145     (case try Toplevel.proof_of state of
 
   146       SOME prf => prf
 
   146       SOME prf => prf
 
   147     | _ => error "No proof state")
 
   147     | _ => error "No proof state")
 
   148 
   148 
   149 fun output_goals  {state = node, ...}  _ = 
   149 fun output_goals  {state = node, context = ctxt, ...} _ = 
   150 let
 
   150 let
 
   151   fun subgoals 0 = ""
 
   151   fun subgoals 0 = ""
 
   152     | subgoals 1 = "goal (1 subgoal):"
 
   152     | subgoals 1 = "goal (1 subgoal):"
 
   153     | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"
 
   153     | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"
 
   154 
   154 
   159   val (As, _) = Logic.strip_horn prop;
 
   159   val (As, _) = Logic.strip_horn prop;
 
   160   val output  = (case (length As) of
 
   160   val output  = (case (length As) of
 
   161                       0 => [goals] 
   161                       0 => [goals] 
   162                     | n => [Pretty.str (subgoals n), goals])  
   162                     | n => [Pretty.str (subgoals n), goals])  
   163 in 
   163 in 
   164   Thy_Output.output output
 
   164   Thy_Output.output ctxt output
 
   165 end
 
   165 end
 
   166 
   166 
   167 fun output_raw_goal_state  {state = node, context = ctxt, ...}  _ = 
   167 fun output_raw_goal_state  {state = node, context = ctxt, ...}  _ = 
   168 let
 
   168 let
 
   169   val state = proof_state node;
 
   169   val state = proof_state node;
 
   171 
   171 
   172   val output  = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))]  
   172   val output  = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))]  
   173   val _ = tracing (Syntax.string_of_term ctxt (prop_of goals))
 
   173   val _ = tracing (Syntax.string_of_term ctxt (prop_of goals))
 
   174   val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals))))
 
   174   val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals))))
 
   175 in 
   175 in 
   176   Thy_Output.output output
 
   176   Thy_Output.output ctxt output
 
   177 end
 
   177 end
 
   178 
   178 
   179 val _ = Thy_Output.antiquotation "subgoals" (Scan.succeed ()) output_goals
 
   179 val _ = Thy_Output.antiquotation "subgoals" (Scan.succeed ()) output_goals
 
   180 val _ = Thy_Output.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state
 
   180 val _ = Thy_Output.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state
 
   181 
   181
isabelle-cookbook