simplified presentation: pass state directly;
authorwenzelm
Sun Mar 08 20:31:54 2009 +0100 (2009-03-08)
changeset 30367ee8841b1b981
parent 30366 e3d788b9dffb
child 30368 1a2a54f910c9
simplified presentation: pass state directly;
src/Pure/Isar/isar_cmd.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Mar 08 20:31:01 2009 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Mar 08 20:31:54 2009 +0100
     1.3 @@ -503,15 +503,15 @@
     1.4  
     1.5  (* markup commands *)
     1.6  
     1.7 -fun check_text (txt, pos) opt_node =
     1.8 +fun check_text (txt, pos) state =
     1.9   (Position.report Markup.doc_source pos;
    1.10 -  ignore (ThyOutput.eval_antiquote (#1 (OuterKeyword.get_lexicons ())) opt_node (txt, pos)));
    1.11 +  ignore (ThyOutput.eval_antiquote (#1 (OuterKeyword.get_lexicons ())) state (txt, pos)));
    1.12  
    1.13  fun header_markup txt = Toplevel.keep (fn state =>
    1.14 -  if Toplevel.is_toplevel state then check_text txt NONE
    1.15 +  if Toplevel.is_toplevel state then check_text txt state
    1.16    else raise Toplevel.UNDEF);
    1.17  
    1.18 -fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (check_text txt o SOME);
    1.19 -fun proof_markup txt = Toplevel.present_proof (check_text txt o SOME);
    1.20 +fun local_theory_markup (loc, txt) = Toplevel.present_local_theory loc (check_text txt);
    1.21 +val proof_markup = Toplevel.present_proof o check_text;
    1.22  
    1.23  end;
     2.1 --- a/src/Pure/Thy/thy_output.ML	Sun Mar 08 20:31:01 2009 +0100
     2.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Mar 08 20:31:54 2009 +0100
     2.3 @@ -11,7 +11,7 @@
     2.4    val indent: int ref
     2.5    val source: bool ref
     2.6    val break: bool ref
     2.7 -  val add_commands: (string * (Args.src -> Toplevel.node option -> string)) list -> unit
     2.8 +  val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
     2.9    val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
    2.10    val defined_command: string -> bool
    2.11    val defined_option: string -> bool
    2.12 @@ -19,10 +19,10 @@
    2.13    val boolean: string -> bool
    2.14    val integer: string -> int
    2.15    val args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
    2.16 -    (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.node option -> string
    2.17 +    (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
    2.18    datatype markup = Markup | MarkupEnv | Verbatim
    2.19    val modes: string list ref
    2.20 -  val eval_antiquote: Scan.lexicon -> Toplevel.node option -> SymbolPos.text * Position.T -> string
    2.21 +  val eval_antiquote: Scan.lexicon -> Toplevel.state -> SymbolPos.text * Position.T -> string
    2.22    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
    2.23      (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
    2.24    val str_of_source: Args.src -> string
    2.25 @@ -57,7 +57,7 @@
    2.26  local
    2.27  
    2.28  val global_commands =
    2.29 -  ref (Symtab.empty: (Args.src -> Toplevel.node option -> string) Symtab.table);
    2.30 +  ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
    2.31  
    2.32  val global_options =
    2.33    ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
    2.34 @@ -81,7 +81,7 @@
    2.35        NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos)
    2.36      | SOME f =>
    2.37         (Position.report (Markup.doc_antiq name) pos;
    2.38 -        (fn node => f src node handle ERROR msg =>
    2.39 +        (fn state => f src state handle ERROR msg =>
    2.40            cat_error msg ("The error(s) above occurred in document antiquotation: " ^
    2.41              quote name ^ Position.str_of pos))))
    2.42    end;
    2.43 @@ -127,10 +127,10 @@
    2.44  
    2.45  fun syntax scan = Args.context_syntax "document antiquotation" scan;
    2.46  
    2.47 -fun args scan f src node : string =
    2.48 +fun args scan f src state : string =
    2.49    let
    2.50      val loc = if ! locale = "" then NONE else SOME (! locale);
    2.51 -    val (x, ctxt) = syntax scan src (Toplevel.presentation_context node loc);
    2.52 +    val (x, ctxt) = syntax scan src (Toplevel.presentation_context_of state loc);
    2.53    in f src ctxt x end;
    2.54  
    2.55  
    2.56 @@ -153,20 +153,20 @@
    2.57  
    2.58  val modes = ref ([]: string list);
    2.59  
    2.60 -fun eval_antiquote lex node (txt, pos) =
    2.61 +fun eval_antiquote lex state (txt, pos) =
    2.62    let
    2.63      fun expand (Antiquote.Text s) = s
    2.64        | expand (Antiquote.Antiq x) =
    2.65            let val (opts, src) = Antiquote.read_antiq lex antiq x in
    2.66 -            options opts (fn () => command src node) ();  (*preview errors!*)
    2.67 +            options opts (fn () => command src state) ();  (*preview errors!*)
    2.68              PrintMode.with_modes (! modes @ Latex.modes)
    2.69 -              (Output.no_warnings (options opts (fn () => command src node))) ()
    2.70 +              (Output.no_warnings (options opts (fn () => command src state))) ()
    2.71            end
    2.72        | expand (Antiquote.Open _) = ""
    2.73        | expand (Antiquote.Close _) = "";
    2.74      val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
    2.75    in
    2.76 -    if is_none node andalso exists Antiquote.is_antiq ants then
    2.77 +    if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
    2.78        error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
    2.79      else implode (map expand ants)
    2.80    end;
    2.81 @@ -187,9 +187,7 @@
    2.82    | VerbatimToken of string * Position.T;
    2.83  
    2.84  fun output_token lex state =
    2.85 -  let
    2.86 -    val eval = eval_antiquote lex (try Toplevel.node_of state)
    2.87 -  in
    2.88 +  let val eval = eval_antiquote lex state in
    2.89      fn NoToken => ""
    2.90       | BasicToken tok => Latex.output_basic tok
    2.91       | MarkupToken (cmd, txt) => Latex.output_markup cmd (eval txt)
    2.92 @@ -511,13 +509,13 @@
    2.93  
    2.94  fun output pretty src ctxt = output_list pretty src ctxt o single;
    2.95  
    2.96 -fun proof_state node =
    2.97 -  (case Option.map Toplevel.proof_node node of
    2.98 -    SOME (SOME prf) => ProofNode.current prf
    2.99 +fun proof_state state =
   2.100 +  (case try Toplevel.proof_of state of
   2.101 +    SOME prf => prf
   2.102    | _ => error "No proof state");
   2.103  
   2.104 -fun output_goals main_goal src node = args (Scan.succeed ()) (output (fn _ => fn _ =>
   2.105 -  Pretty.chunks (Proof.pretty_goals main_goal (proof_state node)))) src node;
   2.106 +fun output_goals main_goal src state = args (Scan.succeed ()) (output (fn _ => fn _ =>
   2.107 +  Pretty.chunks (Proof.pretty_goals main_goal (proof_state state)))) src state;
   2.108  
   2.109  fun ml_val txt = "fn _ => (" ^ txt ^ ");";
   2.110  fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";