src/Pure/Isar/isar_cmd.ML
changeset 59064 a8bcb5a446c8
parent 59029 c907cbe36713
child 59067 dd8ec9138112
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Nov 29 14:43:10 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 30 12:24:56 2014 +0100
     1.3 @@ -6,20 +6,19 @@
     1.4  
     1.5  signature ISAR_CMD =
     1.6  sig
     1.7 -  val global_setup: Symbol_Pos.source -> theory -> theory
     1.8 -  val local_setup: Symbol_Pos.source -> Proof.context -> Proof.context
     1.9 -  val parse_ast_translation: Symbol_Pos.source -> theory -> theory
    1.10 -  val parse_translation: Symbol_Pos.source -> theory -> theory
    1.11 -  val print_translation: Symbol_Pos.source -> theory -> theory
    1.12 -  val typed_print_translation: Symbol_Pos.source -> theory -> theory
    1.13 -  val print_ast_translation: Symbol_Pos.source -> theory -> theory
    1.14 +  val global_setup: Input.source -> theory -> theory
    1.15 +  val local_setup: Input.source -> Proof.context -> Proof.context
    1.16 +  val parse_ast_translation: Input.source -> theory -> theory
    1.17 +  val parse_translation: Input.source -> theory -> theory
    1.18 +  val print_translation: Input.source -> theory -> theory
    1.19 +  val typed_print_translation: Input.source -> theory -> theory
    1.20 +  val print_ast_translation: Input.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.range -> Symbol_Pos.source -> theory -> theory
    1.24 +  val oracle: bstring * Position.range -> Input.source -> theory -> theory
    1.25    val add_defs: (bool * bool) * ((binding * string) * Token.src list) list -> theory -> theory
    1.26 -  val declaration: {syntax: bool, pervasive: bool} ->
    1.27 -    Symbol_Pos.source -> local_theory -> local_theory
    1.28 -  val simproc_setup: string * Position.T -> string list -> Symbol_Pos.source ->
    1.29 +  val declaration: {syntax: bool, pervasive: bool} -> Input.source -> local_theory -> local_theory
    1.30 +  val simproc_setup: string * Position.T -> string list -> Input.source ->
    1.31      string list -> local_theory -> local_theory
    1.32    val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    1.33    val hence: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    1.34 @@ -32,7 +31,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.source -> Toplevel.transition -> Toplevel.transition
    1.39 +  val ml_diag: bool -> Input.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 pretty_theorems: bool -> Toplevel.state -> Pretty.T list
    1.43 @@ -60,13 +59,13 @@
    1.44  
    1.45  fun global_setup source =
    1.46    ML_Lex.read_source false source
    1.47 -  |> ML_Context.expression (#range source) "setup" "theory -> theory"
    1.48 +  |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
    1.49      "Context.map_theory setup"
    1.50    |> Context.theory_map;
    1.51  
    1.52  fun local_setup source =
    1.53    ML_Lex.read_source false source
    1.54 -  |> ML_Context.expression (#range source) "local_setup" "local_theory -> local_theory"
    1.55 +  |> ML_Context.expression (Input.range_of source) "local_setup" "local_theory -> local_theory"
    1.56      "Context.map_proof local_setup"
    1.57    |> Context.proof_map;
    1.58  
    1.59 @@ -75,35 +74,35 @@
    1.60  
    1.61  fun parse_ast_translation source =
    1.62    ML_Lex.read_source false source
    1.63 -  |> ML_Context.expression (#range source) "parse_ast_translation"
    1.64 +  |> ML_Context.expression (Input.range_of source) "parse_ast_translation"
    1.65      "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    1.66      "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
    1.67    |> Context.theory_map;
    1.68  
    1.69  fun parse_translation source =
    1.70    ML_Lex.read_source false source
    1.71 -  |> ML_Context.expression (#range source) "parse_translation"
    1.72 +  |> ML_Context.expression (Input.range_of source) "parse_translation"
    1.73      "(string * (Proof.context -> term list -> term)) list"
    1.74      "Context.map_theory (Sign.parse_translation parse_translation)"
    1.75    |> Context.theory_map;
    1.76  
    1.77  fun print_translation source =
    1.78    ML_Lex.read_source false source
    1.79 -  |> ML_Context.expression (#range source) "print_translation"
    1.80 +  |> ML_Context.expression (Input.range_of source) "print_translation"
    1.81      "(string * (Proof.context -> term list -> term)) list"
    1.82      "Context.map_theory (Sign.print_translation print_translation)"
    1.83    |> Context.theory_map;
    1.84  
    1.85  fun typed_print_translation source =
    1.86    ML_Lex.read_source false source
    1.87 -  |> ML_Context.expression (#range source) "typed_print_translation"
    1.88 +  |> ML_Context.expression (Input.range_of source) "typed_print_translation"
    1.89      "(string * (Proof.context -> typ -> term list -> term)) list"
    1.90      "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
    1.91    |> Context.theory_map;
    1.92  
    1.93  fun print_ast_translation source =
    1.94    ML_Lex.read_source false source
    1.95 -  |> ML_Context.expression (#range source) "print_ast_translation"
    1.96 +  |> ML_Context.expression (Input.range_of source) "print_ast_translation"
    1.97      "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    1.98      "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
    1.99    |> Context.theory_map;
   1.100 @@ -129,7 +128,7 @@
   1.101  
   1.102  fun oracle (name, range) source =
   1.103    let
   1.104 -    val body_range = #range source;
   1.105 +    val body_range = Input.range_of source;
   1.106      val body = ML_Lex.read_source false source;
   1.107  
   1.108      val hidden = ML_Lex.read Position.none;
   1.109 @@ -164,7 +163,7 @@
   1.110  
   1.111  fun declaration {syntax, pervasive} source =
   1.112    ML_Lex.read_source false source
   1.113 -  |> ML_Context.expression (#range source) "declaration" "Morphism.declaration"
   1.114 +  |> ML_Context.expression (Input.range_of source) "declaration" "Morphism.declaration"
   1.115      ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
   1.116        \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
   1.117    |> Context.proof_map;
   1.118 @@ -174,7 +173,7 @@
   1.119  
   1.120  fun simproc_setup name lhss source identifier =
   1.121    ML_Lex.read_source false source
   1.122 -  |> ML_Context.expression (#range source) "proc"
   1.123 +  |> ML_Context.expression (Input.range_of source) "proc"
   1.124      "Morphism.morphism -> Proof.context -> cterm -> thm option"
   1.125      ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
   1.126        \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \