src/Pure/Isar/isar_cmd.ML
changeset 55828 42ac3cfb89f6
parent 53171 a5e54d4d9081
child 56005 4f4fc80b0613
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Mar 01 19:55:01 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Mar 01 22:46:31 2014 +0100
     1.3 @@ -6,20 +6,20 @@
     1.4  
     1.5  signature ISAR_CMD =
     1.6  sig
     1.7 -  val global_setup: Symbol_Pos.text * Position.T -> theory -> theory
     1.8 -  val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context
     1.9 -  val parse_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory
    1.10 -  val parse_translation: Symbol_Pos.text * Position.T -> theory -> theory
    1.11 -  val print_translation: Symbol_Pos.text * Position.T -> theory -> theory
    1.12 -  val typed_print_translation: Symbol_Pos.text * Position.T -> theory -> theory
    1.13 -  val print_ast_translation: Symbol_Pos.text * Position.T -> theory -> theory
    1.14 +  val global_setup: Symbol_Pos.source -> theory -> theory
    1.15 +  val local_setup: Symbol_Pos.source -> Proof.context -> Proof.context
    1.16 +  val parse_ast_translation: Symbol_Pos.source -> theory -> theory
    1.17 +  val parse_translation: Symbol_Pos.source -> theory -> theory
    1.18 +  val print_translation: Symbol_Pos.source -> theory -> theory
    1.19 +  val typed_print_translation: Symbol_Pos.source -> theory -> theory
    1.20 +  val print_ast_translation: Symbol_Pos.source -> theory -> theory
    1.21    val translations: (xstring * string) Syntax.trrule list -> theory -> theory
    1.22    val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
    1.23 -  val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
    1.24 +  val oracle: bstring * Position.T -> Symbol_Pos.source -> theory -> theory
    1.25    val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
    1.26    val declaration: {syntax: bool, pervasive: bool} ->
    1.27 -    Symbol_Pos.text * Position.T -> local_theory -> local_theory
    1.28 -  val simproc_setup: string * Position.T -> string list -> Symbol_Pos.text * Position.T ->
    1.29 +    Symbol_Pos.source -> local_theory -> local_theory
    1.30 +  val simproc_setup: string * Position.T -> string list -> Symbol_Pos.source ->
    1.31      string list -> local_theory -> local_theory
    1.32    val hide_class: bool -> xstring list -> theory -> theory
    1.33    val hide_type: bool -> xstring list -> theory -> theory
    1.34 @@ -36,7 +36,7 @@
    1.35    val immediate_proof: Toplevel.transition -> Toplevel.transition
    1.36    val done_proof: Toplevel.transition -> Toplevel.transition
    1.37    val skip_proof: Toplevel.transition -> Toplevel.transition
    1.38 -  val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    1.39 +  val ml_diag: bool -> Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
    1.40    val diag_state: Proof.context -> Toplevel.state
    1.41    val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
    1.42    val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
    1.43 @@ -56,10 +56,10 @@
    1.44    val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition
    1.45    val print_type: (string list * (string * string option)) ->
    1.46      Toplevel.transition -> Toplevel.transition
    1.47 -  val header_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    1.48 -  val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.text * Position.T) ->
    1.49 +  val header_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
    1.50 +  val local_theory_markup: (xstring * Position.T) option * (Symbol_Pos.source) ->
    1.51      Toplevel.transition -> Toplevel.transition
    1.52 -  val proof_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    1.53 +  val proof_markup: Symbol_Pos.source -> Toplevel.transition -> Toplevel.transition
    1.54  end;
    1.55  
    1.56  structure Isar_Cmd: ISAR_CMD =
    1.57 @@ -70,50 +70,50 @@
    1.58  
    1.59  (* generic setup *)
    1.60  
    1.61 -fun global_setup (txt, pos) =
    1.62 -  ML_Lex.read pos txt
    1.63 -  |> ML_Context.expression pos "val setup: theory -> theory" "Context.map_theory setup"
    1.64 +fun global_setup source =
    1.65 +  ML_Lex.read_source source
    1.66 +  |> ML_Context.expression (#pos source) "val setup: theory -> theory" "Context.map_theory setup"
    1.67    |> Context.theory_map;
    1.68  
    1.69 -fun local_setup (txt, pos) =
    1.70 -  ML_Lex.read pos txt
    1.71 -  |> ML_Context.expression pos "val setup: local_theory -> local_theory" "Context.map_proof setup"
    1.72 +fun local_setup source =
    1.73 +  ML_Lex.read_source source
    1.74 +  |> ML_Context.expression (#pos source) "val setup: local_theory -> local_theory" "Context.map_proof setup"
    1.75    |> Context.proof_map;
    1.76  
    1.77  
    1.78  (* translation functions *)
    1.79  
    1.80 -fun parse_ast_translation (txt, pos) =
    1.81 -  ML_Lex.read pos txt
    1.82 -  |> ML_Context.expression pos
    1.83 +fun parse_ast_translation source =
    1.84 +  ML_Lex.read_source source
    1.85 +  |> ML_Context.expression (#pos source)
    1.86      "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    1.87      "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
    1.88    |> Context.theory_map;
    1.89  
    1.90 -fun parse_translation (txt, pos) =
    1.91 -  ML_Lex.read pos txt
    1.92 -  |> ML_Context.expression pos
    1.93 +fun parse_translation source =
    1.94 +  ML_Lex.read_source source
    1.95 +  |> ML_Context.expression (#pos source)
    1.96      "val parse_translation: (string * (Proof.context -> term list -> term)) list"
    1.97      "Context.map_theory (Sign.parse_translation parse_translation)"
    1.98    |> Context.theory_map;
    1.99  
   1.100 -fun print_translation (txt, pos) =
   1.101 -  ML_Lex.read pos txt
   1.102 -  |> ML_Context.expression pos
   1.103 +fun print_translation source =
   1.104 +  ML_Lex.read_source source
   1.105 +  |> ML_Context.expression (#pos source)
   1.106      "val print_translation: (string * (Proof.context -> term list -> term)) list"
   1.107      "Context.map_theory (Sign.print_translation print_translation)"
   1.108    |> Context.theory_map;
   1.109  
   1.110 -fun typed_print_translation (txt, pos) =
   1.111 -  ML_Lex.read pos txt
   1.112 -  |> ML_Context.expression pos
   1.113 +fun typed_print_translation source =
   1.114 +  ML_Lex.read_source source
   1.115 +  |> ML_Context.expression (#pos source)
   1.116      "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
   1.117      "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
   1.118    |> Context.theory_map;
   1.119  
   1.120 -fun print_ast_translation (txt, pos) =
   1.121 -  ML_Lex.read pos txt
   1.122 -  |> ML_Context.expression pos
   1.123 +fun print_ast_translation source =
   1.124 +  ML_Lex.read_source source
   1.125 +  |> ML_Context.expression (#pos source)
   1.126      "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
   1.127      "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
   1.128    |> Context.theory_map;
   1.129 @@ -135,18 +135,19 @@
   1.130  
   1.131  (* oracles *)
   1.132  
   1.133 -fun oracle (name, pos) (body_txt, body_pos) =
   1.134 +fun oracle (name, pos) source =
   1.135    let
   1.136 -    val body = ML_Lex.read body_pos body_txt;
   1.137 +    val body = ML_Lex.read_source source;
   1.138      val ants =
   1.139        ML_Lex.read Position.none
   1.140         ("local\n\
   1.141          \  val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
   1.142          \  val body = ") @ body @ ML_Lex.read Position.none (";\n\
   1.143          \in\n\
   1.144 -        \  val " ^ name ^ " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
   1.145 +        \  val " ^ name ^
   1.146 +        " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
   1.147          \end;\n");
   1.148 -  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false body_pos ants)) end;
   1.149 +  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false (#pos source) ants)) end;
   1.150  
   1.151  
   1.152  (* old-style defs *)
   1.153 @@ -161,9 +162,9 @@
   1.154  
   1.155  (* declarations *)
   1.156  
   1.157 -fun declaration {syntax, pervasive} (txt, pos) =
   1.158 -  ML_Lex.read pos txt
   1.159 -  |> ML_Context.expression pos
   1.160 +fun declaration {syntax, pervasive} source =
   1.161 +  ML_Lex.read_source source
   1.162 +  |> ML_Context.expression (#pos source)
   1.163      "val declaration: Morphism.declaration"
   1.164      ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
   1.165        \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
   1.166 @@ -172,9 +173,9 @@
   1.167  
   1.168  (* simprocs *)
   1.169  
   1.170 -fun simproc_setup name lhss (txt, pos) identifier =
   1.171 -  ML_Lex.read pos txt
   1.172 -  |> ML_Context.expression pos
   1.173 +fun simproc_setup name lhss source identifier =
   1.174 +  ML_Lex.read_source source
   1.175 +  |> ML_Context.expression (#pos source)
   1.176      "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
   1.177      ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
   1.178        \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
   1.179 @@ -253,11 +254,11 @@
   1.180    fun init _ = Toplevel.toplevel;
   1.181  );
   1.182  
   1.183 -fun ml_diag verbose (txt, pos) = Toplevel.keep (fn state =>
   1.184 +fun ml_diag verbose source = Toplevel.keep (fn state =>
   1.185    let val opt_ctxt =
   1.186      try Toplevel.generic_theory_of state
   1.187      |> Option.map (Context.proof_of #> Diag_State.put state)
   1.188 -  in ML_Context.eval_text_in opt_ctxt verbose pos txt end);
   1.189 +  in ML_Context.eval_source_in opt_ctxt verbose source end);
   1.190  
   1.191  val diag_state = Diag_State.get;
   1.192