clarified signature;
authorwenzelm
Mon Aug 27 20:43:01 2018 +0200 (14 months ago)
changeset 688235e7b1ae10eb8
parent 68822 253f04c1e814
child 68824 7414ce0256e1
clarified signature;
src/Doc/antiquote_setup.ML
src/HOL/ex/Cartouche_Examples.thy
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/method.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_env.ML
src/Pure/ML/ml_lex.ML
src/Pure/Thy/document_antiquotations.ML
src/Pure/Tools/debugger.ML
     1.1 --- a/src/Doc/antiquote_setup.ML	Mon Aug 27 19:29:07 2018 +0200
     1.2 +++ b/src/Doc/antiquote_setup.ML	Mon Aug 27 20:43:01 2018 +0200
     1.3 @@ -71,7 +71,7 @@
     1.4    | _ => error ("Single ML name expected in input: " ^ quote txt));
     1.5  
     1.6  fun prep_ml source =
     1.7 -  (Input.source_content source, ML_Lex.read_source false source);
     1.8 +  (Input.source_content source, ML_Lex.read_source source);
     1.9  
    1.10  fun index_ml name kind ml = Thy_Output.antiquotation_raw name
    1.11    (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
     2.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Mon Aug 27 19:29:07 2018 +0200
     2.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Mon Aug 27 20:43:01 2018 +0200
     2.3 @@ -178,7 +178,7 @@
     2.4        val ctxt' = ctxt |> Context.proof_map
     2.5          (ML_Context.expression (Input.range_of source) "tactic" "Proof.context -> tactic"
     2.6            "Context.map_proof (ML_Tactic.set tactic)"
     2.7 -          (ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source false source));
     2.8 +          (ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source source));
     2.9      in Data.get ctxt' ctxt end;
    2.10  end;
    2.11  \<close>
     3.1 --- a/src/Pure/Isar/attrib.ML	Mon Aug 27 19:29:07 2018 +0200
     3.2 +++ b/src/Pure/Isar/attrib.ML	Mon Aug 27 20:43:01 2018 +0200
     3.3 @@ -215,7 +215,7 @@
     3.4  fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
     3.5  
     3.6  fun attribute_setup name source comment =
     3.7 -  ML_Lex.read_source false source
     3.8 +  ML_Lex.read_source source
     3.9    |> ML_Context.expression (Input.range_of source) "parser" "Thm.attribute context_parser"
    3.10      ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
    3.11        " parser " ^ ML_Syntax.print_string comment ^ ")")
     4.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Aug 27 19:29:07 2018 +0200
     4.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Aug 27 20:43:01 2018 +0200
     4.3 @@ -51,13 +51,13 @@
     4.4  (* generic setup *)
     4.5  
     4.6  fun setup source =
     4.7 -  ML_Lex.read_source false source
     4.8 +  ML_Lex.read_source source
     4.9    |> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
    4.10      "Context.map_theory setup"
    4.11    |> Context.theory_map;
    4.12  
    4.13  fun local_setup source =
    4.14 -  ML_Lex.read_source false source
    4.15 +  ML_Lex.read_source source
    4.16    |> ML_Context.expression (Input.range_of source) "local_setup" "local_theory -> local_theory"
    4.17      "Context.map_proof local_setup"
    4.18    |> Context.proof_map;
    4.19 @@ -66,35 +66,35 @@
    4.20  (* translation functions *)
    4.21  
    4.22  fun parse_ast_translation source =
    4.23 -  ML_Lex.read_source false source
    4.24 +  ML_Lex.read_source source
    4.25    |> ML_Context.expression (Input.range_of source) "parse_ast_translation"
    4.26      "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    4.27      "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
    4.28    |> Context.theory_map;
    4.29  
    4.30  fun parse_translation source =
    4.31 -  ML_Lex.read_source false source
    4.32 +  ML_Lex.read_source source
    4.33    |> ML_Context.expression (Input.range_of source) "parse_translation"
    4.34      "(string * (Proof.context -> term list -> term)) list"
    4.35      "Context.map_theory (Sign.parse_translation parse_translation)"
    4.36    |> Context.theory_map;
    4.37  
    4.38  fun print_translation source =
    4.39 -  ML_Lex.read_source false source
    4.40 +  ML_Lex.read_source source
    4.41    |> ML_Context.expression (Input.range_of source) "print_translation"
    4.42      "(string * (Proof.context -> term list -> term)) list"
    4.43      "Context.map_theory (Sign.print_translation print_translation)"
    4.44    |> Context.theory_map;
    4.45  
    4.46  fun typed_print_translation source =
    4.47 -  ML_Lex.read_source false source
    4.48 +  ML_Lex.read_source source
    4.49    |> ML_Context.expression (Input.range_of source) "typed_print_translation"
    4.50      "(string * (Proof.context -> typ -> term list -> term)) list"
    4.51      "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
    4.52    |> Context.theory_map;
    4.53  
    4.54  fun print_ast_translation source =
    4.55 -  ML_Lex.read_source false source
    4.56 +  ML_Lex.read_source source
    4.57    |> ML_Context.expression (Input.range_of source) "print_ast_translation"
    4.58      "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    4.59      "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
    4.60 @@ -122,7 +122,7 @@
    4.61  fun oracle (name, range) source =
    4.62    let
    4.63      val body_range = Input.range_of source;
    4.64 -    val body = ML_Lex.read_source false source;
    4.65 +    val body = ML_Lex.read_source source;
    4.66  
    4.67      val ants =
    4.68        ML_Lex.read
    4.69 @@ -142,7 +142,7 @@
    4.70  (* declarations *)
    4.71  
    4.72  fun declaration {syntax, pervasive} source =
    4.73 -  ML_Lex.read_source false source
    4.74 +  ML_Lex.read_source source
    4.75    |> ML_Context.expression (Input.range_of source) "declaration" "Morphism.declaration"
    4.76      ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
    4.77        \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
    4.78 @@ -152,7 +152,7 @@
    4.79  (* simprocs *)
    4.80  
    4.81  fun simproc_setup name lhss source =
    4.82 -  ML_Lex.read_source false source
    4.83 +  ML_Lex.read_source source
    4.84    |> ML_Context.expression (Input.range_of source) "proc"
    4.85      "Morphism.morphism -> Proof.context -> cterm -> thm option"
    4.86      ("Context.map_proof (Simplifier.define_simproc_cmd " ^
     5.1 --- a/src/Pure/Isar/method.ML	Mon Aug 27 19:29:07 2018 +0200
     5.2 +++ b/src/Pure/Isar/method.ML	Mon Aug 27 20:43:01 2018 +0200
     5.3 @@ -373,7 +373,7 @@
     5.4              "tactic" "Morphism.morphism -> thm list -> tactic"
     5.5              "Method.set_tactic tactic"
     5.6              (ML_Lex.read "fn morphism: Morphism.morphism => fn facts: thm list =>" @
     5.7 -             ML_Lex.read_source false source);
     5.8 +             ML_Lex.read_source source);
     5.9          val tac = the_tactic context';
    5.10        in
    5.11          fn phi => set_tactic (fn _ => Context.setmp_generic_context (SOME context) (tac phi))
    5.12 @@ -476,7 +476,7 @@
    5.13  fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
    5.14  
    5.15  fun method_setup name source comment =
    5.16 -  ML_Lex.read_source false source
    5.17 +  ML_Lex.read_source source
    5.18    |> ML_Context.expression (Input.range_of source) "parser"
    5.19      "(Proof.context -> Proof.method) context_parser"
    5.20      ("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
     6.1 --- a/src/Pure/ML/ml_context.ML	Mon Aug 27 19:29:07 2018 +0200
     6.2 +++ b/src/Pure/ML/ml_context.ML	Mon Aug 27 20:43:01 2018 +0200
     6.3 @@ -192,7 +192,7 @@
     6.4  
     6.5  fun eval_file flags path =
     6.6    let val pos = Path.position path
     6.7 -  in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
     6.8 +  in eval flags pos (ML_Lex.read_text (File.read path, pos)) end;
     6.9  
    6.10  fun eval_source flags source =
    6.11    let
     7.1 --- a/src/Pure/ML/ml_env.ML	Mon Aug 27 19:29:07 2018 +0200
     7.2 +++ b/src/Pure/ML/ml_env.ML	Mon Aug 27 20:43:01 2018 +0200
     7.3 @@ -174,12 +174,13 @@
     7.4          Name_Space.define (Context.Theory thy') true (Binding.name env_name, (tables, ops)) envs;
     7.5      in envs' end);
     7.6  
     7.7 -fun make_operations SML: operations =
     7.8 - {read_source = ML_Lex.read_source SML,
     7.9 -  explode_token = ML_Lex.explode_content_of SML};
    7.10 +val Isabelle_operations: operations =
    7.11 + {read_source = ML_Lex.read_source,
    7.12 +  explode_token = ML_Lex.check_content_of #> Symbol.explode #> maps (Symbol.esc #> String.explode)};
    7.13  
    7.14 -val Isabelle_operations = make_operations false;
    7.15 -val SML_operations = make_operations true;
    7.16 +val SML_operations: operations =
    7.17 + {read_source = ML_Lex.read_source_sml,
    7.18 +  explode_token = ML_Lex.check_content_of #> String.explode};
    7.19  
    7.20  val _ = Theory.setup (setup Isabelle Isabelle_operations #> setup SML SML_operations);
    7.21  
     8.1 --- a/src/Pure/ML/ml_lex.ML	Mon Aug 27 19:29:07 2018 +0200
     8.2 +++ b/src/Pure/ML/ml_lex.ML	Mon Aug 27 20:43:01 2018 +0200
     8.3 @@ -22,16 +22,18 @@
     8.4    val kind_of: token -> token_kind
     8.5    val content_of: token -> string
     8.6    val check_content_of: token -> string
     8.7 -  val explode_content_of: bool -> token -> char list
     8.8    val flatten: token list -> string
     8.9    val source: (Symbol.symbol, 'a) Source.source ->
    8.10      (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
    8.11        Source.source) Source.source
    8.12    val tokenize: string -> token list
    8.13 -  val read_pos: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
    8.14 +  val read_text: Symbol_Pos.text * Position.T -> token Antiquote.antiquote list
    8.15    val read: Symbol_Pos.text -> token Antiquote.antiquote list
    8.16    val read_set_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list
    8.17 -  val read_source: bool -> Input.source -> token Antiquote.antiquote list
    8.18 +  val read_source': {language: bool -> Markup.T, opaque_warning: bool, symbols: bool} ->
    8.19 +    token Antiquote.antiquote Symbol_Pos.scanner -> Input.source -> token Antiquote.antiquote list
    8.20 +  val read_source: Input.source -> token Antiquote.antiquote list
    8.21 +  val read_source_sml: Input.source -> token Antiquote.antiquote list
    8.22  end;
    8.23  
    8.24  structure ML_Lex: ML_LEX =
    8.25 @@ -115,7 +117,7 @@
    8.26  fun is_comment (Token (_, (Comment _, _))) = true
    8.27    | is_comment _ = false;
    8.28  
    8.29 -fun warn tok =
    8.30 +fun warning_opaque tok =
    8.31    (case tok of
    8.32      Token (_, (Keyword, ":>")) =>
    8.33        warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
    8.34 @@ -128,10 +130,6 @@
    8.35      Error msg => error msg
    8.36    | _ => content_of tok);
    8.37  
    8.38 -fun explode_content_of SML =
    8.39 -  check_content_of #>
    8.40 -  (if SML then String.explode else Symbol.explode #> maps (Symbol.esc #> String.explode));
    8.41 -
    8.42  
    8.43  (* flatten *)
    8.44  
    8.45 @@ -310,12 +308,14 @@
    8.46      scan_ident >> token Ident ||
    8.47      scan_type_var >> token Type_Var);
    8.48  
    8.49 +val scan_sml_antiq = scan_sml >> Antiquote.Text;
    8.50 +
    8.51  val scan_ml_antiq =
    8.52    Comment.scan >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
    8.53    Antiquote.scan_control >> Antiquote.Control ||
    8.54    Antiquote.scan_antiq >> Antiquote.Antiq ||
    8.55    scan_rat_antiq >> Antiquote.Antiq ||
    8.56 -  scan_sml >> Antiquote.Text;
    8.57 +  scan_sml_antiq;
    8.58  
    8.59  fun recover msg =
    8.60   (recover_char ||
    8.61 @@ -325,12 +325,8 @@
    8.62    Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
    8.63    >> (single o token (Error msg));
    8.64  
    8.65 -fun gen_read SML pos text =
    8.66 +fun reader {opaque_warning} scan syms =
    8.67    let
    8.68 -    val syms =
    8.69 -      Symbol_Pos.explode (text, pos)
    8.70 -      |> SML ? maps (fn (s, p) => raw_explode s |> map (rpair p));
    8.71 -
    8.72      val termination =
    8.73        if null syms then []
    8.74        else
    8.75 @@ -339,8 +335,8 @@
    8.76            val pos2 = Position.advance Symbol.space pos1;
    8.77          in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end;
    8.78  
    8.79 -    val scan = if SML then scan_sml >> Antiquote.Text else scan_ml_antiq;
    8.80 -    fun check (Antiquote.Text tok) = (check_content_of tok; if SML then () else warn tok)
    8.81 +    fun check (Antiquote.Text tok) =
    8.82 +          (check_content_of tok; if opaque_warning then warning_opaque tok else ())
    8.83        | check _ = ();
    8.84      val input =
    8.85        Source.of_list syms
    8.86 @@ -361,22 +357,31 @@
    8.87  
    8.88  val tokenize = Symbol.explode #> Source.of_list #> source #> Source.exhaust;
    8.89  
    8.90 -val read_pos = gen_read false;
    8.91 -
    8.92 -val read = read_pos Position.none;
    8.93 +val read_text = reader {opaque_warning = true} scan_ml_antiq o Symbol_Pos.explode;
    8.94 +fun read text = read_text (text, Position.none);
    8.95  
    8.96  fun read_set_range range =
    8.97    read #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq);
    8.98  
    8.99 -fun read_source SML source =
   8.100 +fun read_source' {language, symbols, opaque_warning} scan source =
   8.101    let
   8.102      val pos = Input.pos_of source;
   8.103 -    val language = if SML then Markup.language_SML else Markup.language_ML;
   8.104      val _ =
   8.105        if Position.is_reported_range pos
   8.106        then Position.report pos (language (Input.is_delimited source))
   8.107        else ();
   8.108 -  in gen_read SML pos (Input.text_of source) end;
   8.109 +    val syms =
   8.110 +      Symbol_Pos.explode (Input.text_of source, pos)
   8.111 +      |> not symbols ? maps (fn (s, p) => raw_explode s |> map (rpair p));
   8.112 +  in reader {opaque_warning = opaque_warning} scan syms end;
   8.113 +
   8.114 +val read_source =
   8.115 +  read_source' {language = Markup.language_ML, symbols = true, opaque_warning = true}
   8.116 +    scan_ml_antiq;
   8.117 +
   8.118 +val read_source_sml =
   8.119 +  read_source' {language = Markup.language_SML, symbols = false, opaque_warning = false}
   8.120 +    scan_sml_antiq;
   8.121  
   8.122  end;
   8.123  
     9.1 --- a/src/Pure/Thy/document_antiquotations.ML	Mon Aug 27 19:29:07 2018 +0200
     9.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Mon Aug 27 20:43:01 2018 +0200
     9.3 @@ -264,7 +264,7 @@
     9.4        in Input.source_content text end);
     9.5  
     9.6  fun ml_enclose bg en source =
     9.7 -  ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
     9.8 +  ML_Lex.read bg @ ML_Lex.read_source source @ ML_Lex.read en;
     9.9  
    9.10  in
    9.11  
    10.1 --- a/src/Pure/Tools/debugger.ML	Mon Aug 27 19:29:07 2018 +0200
    10.2 +++ b/src/Pure/Tools/debugger.ML	Mon Aug 27 20:43:01 2018 +0200
    10.3 @@ -131,18 +131,19 @@
    10.4      "Context.put_generic_context (SOME (Context.Proof ML_context))",
    10.5      "Context.put_generic_context (SOME ML_context)"];
    10.6  
    10.7 -fun make_environment sml = if sml then ML_Env.SML else ML_Env.Isabelle;
    10.8 +fun environment SML = if SML then ML_Env.SML else ML_Env.Isabelle;
    10.9 +fun operations SML = if SML then ML_Env.SML_operations else ML_Env.Isabelle_operations;
   10.10  
   10.11  fun evaluate {SML, verbose} =
   10.12    ML_Context.eval
   10.13 -    {environment = make_environment SML, redirect = false, verbose = verbose,
   10.14 +    {environment = environment SML, redirect = false, verbose = verbose,
   10.15        debug = SOME false, writeln = writeln_message, warning = warning_message}
   10.16      Position.none;
   10.17  
   10.18  fun eval_setup thread_name index SML context =
   10.19    context
   10.20    |> Context_Position.set_visible_generic false
   10.21 -  |> ML_Env.add_name_space (make_environment SML)
   10.22 +  |> ML_Env.add_name_space (environment SML)
   10.23        (PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index));
   10.24  
   10.25  fun eval_context thread_name index SML toks =
   10.26 @@ -170,13 +171,13 @@
   10.27  
   10.28  fun eval thread_name index SML txt1 txt2 =
   10.29    let
   10.30 -    val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
   10.31 +    val (toks1, toks2) = apply2 (#read_source (operations SML) o Input.string) (txt1, txt2);
   10.32      val context = eval_context thread_name index SML toks1;
   10.33    in Context.setmp_generic_context (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end;
   10.34  
   10.35  fun print_vals thread_name index SML txt =
   10.36    let
   10.37 -    val toks = ML_Lex.read_source SML (Input.string txt)
   10.38 +    val toks = #read_source (operations SML) (Input.string txt)
   10.39      val context = eval_context thread_name index SML toks;
   10.40      val space = PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index);
   10.41