src/Pure/Isar/isar_cmd.ML
changeset 37305 9763792e4ac7
parent 37216 3165bc303f66
child 37866 cd1d1bc7684c
equal deleted inserted replaced
37304:645f849eefa7 37305:9763792e4ac7
    40   val quit: Toplevel.transition -> Toplevel.transition
    40   val quit: Toplevel.transition -> Toplevel.transition
    41   val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
    41   val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
    42   val disable_pr: Toplevel.transition -> Toplevel.transition
    42   val disable_pr: Toplevel.transition -> Toplevel.transition
    43   val enable_pr: Toplevel.transition -> Toplevel.transition
    43   val enable_pr: Toplevel.transition -> Toplevel.transition
    44   val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    44   val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
       
    45   val diag_state: unit -> Toplevel.state
       
    46   val diag_goal: unit -> {context: Proof.context, facts: thm list, goal: thm}
    45   val cd: Path.T -> Toplevel.transition -> Toplevel.transition
    47   val cd: Path.T -> Toplevel.transition -> Toplevel.transition
    46   val pwd: Toplevel.transition -> Toplevel.transition
    48   val pwd: Toplevel.transition -> Toplevel.transition
    47   val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
    49   val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
    48   val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
    50   val print_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
    49   val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
    51   val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
   297 val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
   299 val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
   298 
   300 
   299 
   301 
   300 (* diagnostic ML evaluation *)
   302 (* diagnostic ML evaluation *)
   301 
   303 
       
   304 structure Diag_State = Proof_Data
       
   305 (
       
   306   type T = Toplevel.state;
       
   307   fun init _ = Toplevel.toplevel;
       
   308 );
       
   309 
   302 fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state =>
   310 fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state =>
   303   (ML_Context.eval_text_in
   311   let val opt_ctxt =
   304     (Option.map Context.proof_of (try Toplevel.generic_theory_of state)) verbose pos txt));
   312     try Toplevel.generic_theory_of state
       
   313     |> Option.map (Context.proof_of #> Diag_State.put state)
       
   314   in ML_Context.eval_text_in opt_ctxt verbose pos txt end);
       
   315 
       
   316 fun diag_state () = Diag_State.get (ML_Context.the_local_context ());
       
   317 
       
   318 fun diag_goal () =
       
   319   Proof.goal (Toplevel.proof_of (diag_state ()))
       
   320     handle Toplevel.UNDEF => error "No goal present";
       
   321 
       
   322 val _ = ML_Antiquote.value "Isar.state" (Scan.succeed "Isar_Cmd.diag_state ()");
       
   323 val _ = ML_Antiquote.value "Isar.goal" (Scan.succeed "Isar_Cmd.diag_goal ()");
   305 
   324 
   306 
   325 
   307 (* current working directory *)
   326 (* current working directory *)
   308 
   327 
   309 fun cd path = Toplevel.imperative (fn () => File.cd path);
   328 fun cd path = Toplevel.imperative (fn () => File.cd path);