diff --git a/src/Pure/General/completion.ML b/src/Pure/General/completion.ML --- a/src/Pure/General/completion.ML +++ b/src/Pure/General/completion.ML @@ -1,102 +1,107 @@ (* Title: Pure/General/completion.ML Author: Makarius Semantic completion within the formal context. *) signature COMPLETION = sig type name = string * (string * string) type T val names: Position.T -> name list -> T val none: T val make: string * Position.T -> ((string -> bool) -> name list) -> T val encode: T -> XML.body val markup_element: T -> (Markup.T * XML.body) option val markup_report: T list -> string val make_report: string * Position.T -> ((string -> bool) -> name list) -> string val suppress_abbrevs: string -> Markup.T list + val check_item: string -> (string * 'a -> Markup.T) -> + (string * 'a) list -> Proof.context -> string * Position.T -> string + val check_entity: string -> (string * Position.T) list -> + Proof.context -> string * Position.T -> string val check_option: Options.T -> Proof.context -> string * Position.T -> string val check_option_value: Proof.context -> string * Position.T -> string * Position.T -> Options.T -> string * Options.T end; structure Completion: COMPLETION = struct (* completion of names *) type name = string * (string * string); (*external name, kind, internal name*) abstype T = Completion of {pos: Position.T, total: int, names: name list} with fun dest (Completion args) = args; fun names pos names = Completion {pos = pos, total = length names, names = take (Options.default_int "completion_limit") names}; end; val none = names Position.none []; fun make (name, pos) make_names = if Position.is_reported pos andalso name <> "" andalso name <> "_" then names pos (make_names (String.isPrefix (Name.clean name))) else none; fun encode completion = let val {total, names, ...} = dest completion; open XML.Encode; in pair int (list (pair string (pair string string))) (total, names) end; fun markup_element completion = let val {pos, names, ...} = dest completion in if Position.is_reported pos andalso not (null names) then SOME (Position.markup pos Markup.completion, encode completion) else NONE end; val markup_report = map_filter markup_element #> map XML.Elem #> YXML.string_of_body #> Markup.markup_report; val make_report = markup_report oo (single oo make); (* suppress short abbreviations *) fun suppress_abbrevs s = if not (Symbol.is_ascii_identifier s) andalso (length (Symbol.explode s) <= 1 orelse s = "::") then [Markup.no_completion] else []; -(* system options *) +(* check items *) -fun check_option options ctxt (name, pos) = - let - val markup = - Options.markup options (name, pos) handle ERROR msg => - let - val completion_report = - make_report (name, pos) (fn completed => - Options.names options - |> filter completed - |> map (fn a => (a, ("system_option", a)))); - in error (msg ^ completion_report) end; - val _ = Context_Position.report ctxt pos markup; - in name end; +fun check_item kind markup items ctxt (name, pos) = + (case AList.lookup (op =) items name of + SOME x => (Context_Position.report ctxt pos (markup (name, x)); name) + | NONE => + let + fun make_names completed = + map_filter (fn (a, _) => if completed a then SOME (a, (kind, a)) else NONE) items; + val completion_report = make_report (name, pos) make_names; + in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end); + +fun check_entity kind = check_item kind (Position.entity_markup kind); + + +val check_option = check_entity Markup.system_optionN o Options.dest; fun check_option_value ctxt (name, pos) (value, pos') options = let val _ = check_option options ctxt (name, pos); val options' = Options.update name value options handle ERROR msg => error (msg ^ Position.here pos'); in (name, options') end; end; diff --git a/src/Pure/PIDE/resources.ML b/src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML +++ b/src/Pure/PIDE/resources.ML @@ -1,324 +1,312 @@ (* Title: Pure/PIDE/resources.ML Author: Makarius Resources for theories and auxiliary files. *) signature RESOURCES = sig val default_qualifier: string val init_session: {pide: bool, session_positions: (string * Properties.T) list, session_directories: (string * string) list, docs: string list, global_theories: (string * string) list, loaded_theories: string list} -> unit val finish_session_base: unit -> unit val is_pide: unit -> bool val global_theory: string -> string option val loaded_theory: string -> bool val check_session: Proof.context -> string * Position.T -> string val check_doc: Proof.context -> string * Position.T -> string val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val thy_path: Path.T -> Path.T val theory_qualifier: string -> string val find_theory_file: string -> Path.T option val import_name: string -> Path.T -> string -> {node_name: Path.T, master_dir: Path.T, theory_name: string} val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, imports: (string * Position.T) list, keywords: Thy_Header.keywords} val parse_files: string -> (theory -> Token.file list) parser val provide: Path.T * SHA1.digest -> theory -> theory val provide_file: Token.file -> theory -> theory val provide_parse_files: string -> (theory -> Token.file list * theory) parser val loaded_files_current: theory -> bool val check_path: Proof.context -> Path.T option -> string * Position.T -> Path.T val check_file: Proof.context -> Path.T option -> string * Position.T -> Path.T val check_dir: Proof.context -> Path.T option -> string * Position.T -> Path.T end; structure Resources: RESOURCES = struct (* session base *) val default_qualifier = "Draft"; type entry = {pos: Position.T, serial: serial}; fun make_entry props : entry = {pos = Position.of_properties props, serial = serial ()}; val empty_session_base = {pide = false, session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, docs = []: (string * entry) list, global_theories = Symtab.empty: string Symtab.table, loaded_theories = Symtab.empty: unit Symtab.table}; val global_session_base = Synchronized.var "Sessions.base" empty_session_base; fun init_session {pide, session_positions, session_directories, docs, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => {pide = pide, session_positions = sort_by #1 (map (apsnd make_entry) session_positions), session_directories = fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir)) session_directories Symtab.empty, docs = sort_by #1 (map (apsnd make_entry o rpair []) docs), global_theories = Symtab.make global_theories, loaded_theories = Symtab.make_set loaded_theories}); fun finish_session_base () = Synchronized.change global_session_base (fn {global_theories, loaded_theories, ...} => {pide = false, session_positions = [], session_directories = Symtab.empty, docs = [], global_theories = global_theories, loaded_theories = loaded_theories}); fun get_session_base f = f (Synchronized.value global_session_base); fun is_pide () = get_session_base #pide; fun global_theory a = Symtab.lookup (get_session_base #global_theories) a; fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a; + fun check_name which kind markup ctxt (name, pos) = - let val entries = get_session_base which in - (case AList.lookup (op =) entries name of - SOME entry => (Context_Position.report ctxt pos (markup name entry); name) - | NONE => - let - val completion_report = - Completion.make_report (name, pos) - (fn completed => - entries - |> map #1 - |> filter completed - |> sort_strings - |> map (fn a => (a, (kind, a)))); - in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end) - end; + Completion.check_item kind markup (get_session_base which |> sort_by #1) ctxt (name, pos); -fun markup_session name {pos, serial} = - Markup.properties - (Position.entity_properties_of false serial pos) (Markup.entity Markup.sessionN name); +val check_session = + check_name #session_positions "session" + (fn (name, {pos, serial}) => + Markup.entity Markup.sessionN name + |> Markup.properties (Position.entity_properties_of false serial pos)); -val check_session = check_name #session_positions "session" markup_session; -val check_doc = check_name #docs "documentation" (fn name => fn _ => Markup.doc name); +val check_doc = check_name #docs "documentation" (Markup.doc o #1); (* manage source files *) type files = {master_dir: Path.T, (*master directory of theory source*) imports: (string * Position.T) list, (*source specification of imports*) provided: (Path.T * SHA1.digest) list}; (*source path, digest*) fun make_files (master_dir, imports, provided): files = {master_dir = master_dir, imports = imports, provided = provided}; structure Files = Theory_Data ( type T = files; val empty = make_files (Path.current, [], []); fun extend _ = empty; fun merge _ = empty; ); fun map_files f = Files.map (fn {master_dir, imports, provided} => make_files (f (master_dir, imports, provided))); val master_directory = #master_dir o Files.get; val imports_of = #imports o Files.get; fun begin_theory master_dir {name, imports, keywords} parents = Theory.begin_theory name parents |> map_files (fn _ => (Path.explode (Path.smart_implode master_dir), imports, [])) |> Thy_Header.add_keywords keywords; (* theory files *) val thy_path = Path.ext "thy"; fun theory_qualifier theory = (case global_theory theory of SOME qualifier => qualifier | NONE => Long_Name.qualifier theory); fun theory_name qualifier theory = if Long_Name.is_qualified theory orelse is_some (global_theory theory) then theory else Long_Name.qualify qualifier theory; fun find_theory_file thy_name = let val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name)); val session = theory_qualifier thy_name; val dirs = Symtab.lookup_list (get_session_base #session_directories) session; in dirs |> get_first (fn dir => let val path = Path.append dir thy_file in if File.is_file path then SOME path else NONE end) end; fun make_theory_node node_name theory = {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory}; fun loaded_theory_node theory = {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}; fun import_name qualifier dir s = let val theory = theory_name qualifier (Thy_Header.import_name s); fun theory_node () = make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory; in if not (Thy_Header.is_base_name s) then theory_node () else if loaded_theory theory then loaded_theory_node theory else (case find_theory_file theory of SOME node_name => make_theory_node node_name theory | NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ()) end; fun check_file dir file = File.check_file (File.full_path dir file); fun check_thy dir thy_name = let val thy_base_name = Long_Name.base_name thy_name; val master_file = (case find_theory_file thy_name of SOME path => check_file Path.current path | NONE => check_file dir (thy_path (Path.basic thy_base_name))); val text = File.read master_file; val {name = (name, pos), imports, keywords} = Thy_Header.read (Path.position master_file) text; val _ = thy_base_name <> name andalso error ("Bad theory name " ^ quote name ^ " for file " ^ Path.print (Path.base master_file) ^ Position.here pos); in {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, imports = imports, keywords = keywords} end; (* load files *) fun parse_files cmd = Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy => (case Token.get_files tok of [] => let val keywords = Thy_Header.get_keywords thy; val master_dir = master_directory thy; val pos = Token.pos_of tok; val src_paths = Keyword.command_files keywords cmd (Path.explode name); in map (Command.read_file master_dir pos) src_paths end | files => map Exn.release files)); fun provide (src_path, id) = map_files (fn (master_dir, imports, provided) => if AList.defined (op =) provided src_path then error ("Duplicate use of source file: " ^ Path.print src_path) else (master_dir, imports, (src_path, id) :: provided)); fun provide_file (file: Token.file) = provide (#src_path file, #digest file); fun provide_parse_files cmd = parse_files cmd >> (fn files => fn thy => let val fs = files thy; val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy; in (fs, thy') end); fun load_file thy src_path = let val full_path = check_file (master_directory thy) src_path; val text = File.read full_path; val id = SHA1.digest text; in ((full_path, id), text) end; fun loaded_files_current thy = #provided (Files.get thy) |> forall (fn (src_path, id) => (case try (load_file thy) src_path of NONE => false | SOME ((_, id'), _) => id = id')); (* formal check *) fun formal_check check_file ctxt opt_dir (name, pos) = let fun err msg = error (msg ^ Position.here pos); val _ = Context_Position.report ctxt pos Markup.language_path; val dir = (case opt_dir of SOME dir => dir | NONE => master_directory (Proof_Context.theory_of ctxt)); val path = Path.append dir (Path.explode name) handle ERROR msg => err msg; val _ = Path.expand path handle ERROR msg => err msg; val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path)); val _ = check_file path handle ERROR msg => err msg; in path end; val check_path = formal_check I; val check_file = formal_check File.check_file; val check_dir = formal_check File.check_dir; (* antiquotations *) local fun document_antiq (check: Proof.context -> Path.T option -> string * Position.T -> Path.T) = Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) => let val _ = check ctxt NONE (name, pos); val latex = Latex.string (Latex.output_ascii_breakable "/" name); in Latex.enclose_block "\\isatt{" "}" [latex] end); fun ML_antiq check = Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) => check ctxt (SOME Path.current) (name, pos) |> ML_Syntax.print_path); in val _ = Theory.setup (Thy_Output.antiquotation_verbatim_embedded \<^binding>\session\ (Scan.lift Parse.embedded_position) check_session #> Thy_Output.antiquotation_verbatim_embedded \<^binding>\doc\ (Scan.lift Parse.embedded_position) check_doc #> Thy_Output.antiquotation_raw_embedded \<^binding>\path\ (document_antiq check_path) (K I) #> Thy_Output.antiquotation_raw_embedded \<^binding>\file\ (document_antiq check_file) (K I) #> Thy_Output.antiquotation_raw_embedded \<^binding>\dir\ (document_antiq check_dir) (K I) #> ML_Antiquotation.value_embedded \<^binding>\path\ (ML_antiq check_path) #> ML_Antiquotation.value_embedded \<^binding>\file\ (ML_antiq check_file) #> ML_Antiquotation.value_embedded \<^binding>\dir\ (ML_antiq check_dir) #> ML_Antiquotation.value_embedded \<^binding>\path_binding\ (Scan.lift (Parse.position Parse.path) >> (ML_Syntax.print_path_binding o Path.explode_binding)) #> ML_Antiquotation.value \<^binding>\master_dir\ (Args.theory >> (ML_Syntax.print_path o master_directory))); end; end; diff --git a/src/Pure/System/isabelle_system.ML b/src/Pure/System/isabelle_system.ML --- a/src/Pure/System/isabelle_system.ML +++ b/src/Pure/System/isabelle_system.ML @@ -1,137 +1,123 @@ (* Title: Pure/System/isabelle_system.ML Author: Makarius Isabelle system support. *) signature ISABELLE_SYSTEM = sig val bash_output_check: string -> string val bash_output: string -> string * int val bash: string -> int val bash_functions: unit -> string list val check_bash_function: Proof.context -> string * Position.T -> string val rm_tree: Path.T -> unit val mkdirs: Path.T -> unit val mkdir: Path.T -> unit val copy_dir: Path.T -> Path.T -> unit val copy_file: Path.T -> Path.T -> unit val copy_file_base: Path.T * Path.T -> Path.T -> unit val create_tmp_path: string -> string -> Path.T val with_tmp_file: string -> string -> (Path.T -> 'a) -> 'a val with_tmp_dir: string -> (Path.T -> 'a) -> 'a end; structure Isabelle_System: ISABELLE_SYSTEM = struct (* bash *) fun bash_output_check s = (case Bash.process s of {rc = 0, out, ...} => (trim_line out) | {err, ...} => error (trim_line err)); fun bash_output s = let val {out, err, rc, ...} = Bash.process s; val _ = warning (trim_line err); in (out, rc) end; fun bash s = let val (out, rc) = bash_output s; val _ = writeln (trim_line out); in rc end; (* bash functions *) fun bash_functions () = bash_output_check "declare -Fx" |> split_lines |> map_filter (space_explode " " #> try List.last); -fun check_bash_function ctxt (name, pos) = - let - val kind = Markup.bash_functionN; - val funs = bash_functions (); - in - if member (op =) funs name then - (Context_Position.report ctxt pos (Markup.bash_function name); name) - else - let - val completion_report = - Completion.make_report (name, pos) - (fn completed => - filter completed funs - |> sort_strings - |> map (fn a => (a, (kind, a)))); - in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end - end; +fun check_bash_function ctxt arg = + Completion.check_item Markup.bash_functionN (Markup.bash_function o #1) + (bash_functions () |> map (rpair ())) ctxt arg; (* directory operations *) fun system_command cmd = if bash cmd <> 0 then error ("System command failed: " ^ cmd) else (); fun rm_tree path = system_command ("rm -r -f " ^ File.bash_path path); fun mkdirs path = if File.is_dir path then () else (bash ("perl -e \"use File::Path make_path; make_path('" ^ File.standard_path path ^ "');\""); if File.is_dir path then () else error ("Failed to create directory: " ^ Path.print path)); fun mkdir path = if File.is_dir path then () else OS.FileSys.mkDir (File.platform_path path); fun copy_dir src dst = if File.eq (src, dst) then () else (system_command ("cp -p -R -f " ^ File.bash_path src ^ "/. " ^ File.bash_path dst); ()); fun copy_file src0 dst0 = let val src = Path.expand src0; val dst = Path.expand dst0; val target = if File.is_dir dst then Path.append dst (Path.base src) else dst; in if File.eq (src, target) then () else ignore (system_command ("cp -p -f " ^ File.bash_path src ^ " " ^ File.bash_path target)) end; fun copy_file_base (base_dir, src0) target_dir = let val src = Path.expand src0; val src_dir = Path.dir src; val _ = if Path.starts_basic src then () else error ("Illegal path specification " ^ Path.print src ^ " beyond base directory"); val _ = mkdirs (Path.append target_dir src_dir); in copy_file (Path.append base_dir src) (Path.append target_dir src) end; (* tmp files *) fun create_tmp_path name ext = let val path = File.tmp_path (Path.basic (name ^ serial_string ()) |> Path.ext ext); val _ = File.exists path andalso raise Fail ("Temporary file already exists: " ^ Path.print path); in path end; fun with_tmp_file name ext f = let val path = create_tmp_path name ext in Exn.release (Exn.capture f path before ignore (try File.rm path)) end; (* tmp dirs *) fun with_tmp_dir name f = let val path = create_tmp_path name ""; val _ = mkdirs path; in Exn.release (Exn.capture f path before ignore (try rm_tree path)) end; end; diff --git a/src/Pure/System/options.ML b/src/Pure/System/options.ML --- a/src/Pure/System/options.ML +++ b/src/Pure/System/options.ML @@ -1,225 +1,213 @@ (* Title: Pure/System/options.ML Author: Makarius System options with external string representation. *) signature OPTIONS = sig val boolT: string val intT: string val realT: string val stringT: string val unknownT: string type T val empty: T - val names: T -> string list - val markup: T -> string * Position.T -> Markup.T + val dest: T -> (string * Position.T) list val typ: T -> string -> string val bool: T -> string -> bool val int: T -> string -> int val real: T -> string -> real val seconds: T -> string -> Time.time val string: T -> string -> string val put_bool: string -> bool -> T -> T val put_int: string -> int -> T -> T val put_real: string -> real -> T -> T val put_string: string -> string -> T -> T val declare: {pos: Position.T, name: string, typ: string, value: string} -> T -> T val update: string -> string -> T -> T val decode: XML.body -> T val default: unit -> T - val default_markup: string * Position.T -> Markup.T val default_typ: string -> string val default_bool: string -> bool val default_int: string -> int val default_real: string -> real val default_seconds: string -> Time.time val default_string: string -> string val default_put_bool: string -> bool -> unit val default_put_int: string -> int -> unit val default_put_real: string -> real -> unit val default_put_string: string -> string -> unit val get_default: string -> string val put_default: string -> string -> unit val set_default: T -> unit val reset_default: unit -> unit val load_default: unit -> unit end; structure Options: OPTIONS = struct (* representation *) val boolT = "bool"; val intT = "int"; val realT = "real"; val stringT = "string"; val unknownT = "unknown"; datatype T = Options of {pos: Position.T, typ: string, value: string} Symtab.table; val empty = Options Symtab.empty; -fun names (Options tab) = sort_strings (Symtab.keys tab); +fun dest (Options tab) = + Symtab.fold (fn (name, {pos, ...}) => cons (name, pos)) tab [] + |> sort_by #1; (* check *) fun check_name (Options tab) name = let val opt = Symtab.lookup tab name in if is_some opt andalso #typ (the opt) <> unknownT then the opt else error ("Unknown system option " ^ quote name) end; fun check_type options name typ = let val opt = check_name options name in if #typ opt = typ then opt else error ("Ill-typed system option " ^ quote name ^ " : " ^ #typ opt ^ " vs. " ^ typ) end; -(* markup *) - -fun markup options (name, pos) = - let - val opt = - check_name options name - handle ERROR msg => error (msg ^ Position.here pos); - val props = Position.def_properties_of (#pos opt); - in Markup.properties props (Markup.entity Markup.system_optionN name) end; - - (* typ *) fun typ options name = #typ (check_name options name); (* basic operations *) fun put T print name x (options as Options tab) = let val opt = check_type options name T in Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = print x}) tab) end; fun get T parse options name = let val opt = check_type options name T in (case parse (#value opt) of SOME x => x | NONE => error ("Malformed value for system option " ^ quote name ^ " : " ^ T ^ " =\n" ^ quote (#value opt))) end; (* internal lookup and update *) val bool = get boolT (try Value.parse_bool); val int = get intT (try Value.parse_int); val real = get realT (try Value.parse_real); val seconds = Time.fromReal oo real; val string = get stringT SOME; val put_bool = put boolT Value.print_bool; val put_int = put intT Value.print_int; val put_real = put realT Value.print_real; val put_string = put stringT I; (* external updates *) fun check_value options name = let val opt = check_name options name in if #typ opt = boolT then ignore (bool options name) else if #typ opt = intT then ignore (int options name) else if #typ opt = realT then ignore (real options name) else if #typ opt = stringT then ignore (string options name) else () end; fun declare {pos, name, typ, value} (Options tab) = let val options' = (case Symtab.lookup tab name of SOME other => error ("Duplicate declaration of system option " ^ quote name ^ Position.here pos ^ Position.here (#pos other)) | NONE => Options (Symtab.update (name, {pos = pos, typ = typ, value = value}) tab)); val _ = typ = boolT orelse typ = intT orelse typ = realT orelse typ = stringT orelse error ("Unknown type for system option " ^ quote name ^ " : " ^ quote typ ^ Position.here pos); val _ = check_value options' name; in options' end; fun update name value (options as Options tab) = let val opt = check_name options name; val options' = Options (Symtab.update (name, {pos = #pos opt, typ = #typ opt, value = value}) tab); val _ = check_value options' name; in options' end; (* decode *) fun decode_opt body = let open XML.Decode in list (pair properties (pair string (pair string string))) end body |> map (fn (props, (name, (typ, value))) => {pos = Position.of_properties props, name = name, typ = typ, value = value}); fun decode body = fold declare (decode_opt body) empty; (** global default **) val global_default = Synchronized.var "Options.default" (NONE: T option); fun err_no_default () = error "Missing default for system options within Isabelle process"; fun change_default f x y = Synchronized.change global_default (fn SOME options => SOME (f x y options) | NONE => err_no_default ()); fun default () = (case Synchronized.value global_default of SOME options => options | NONE => err_no_default ()); -fun default_markup arg = markup (default ()) arg; fun default_typ name = typ (default ()) name; fun default_bool name = bool (default ()) name; fun default_int name = int (default ()) name; fun default_real name = real (default ()) name; fun default_seconds name = seconds (default ()) name; fun default_string name = string (default ()) name; val default_put_bool = change_default put_bool; val default_put_int = change_default put_int; val default_put_real = change_default put_real; val default_put_string = change_default put_string; fun get_default name = let val options = default () in get (typ options name) SOME options name end; val put_default = change_default update; fun set_default options = Synchronized.change global_default (K (SOME options)); fun reset_default () = Synchronized.change global_default (K NONE); fun load_default () = (case getenv "ISABELLE_PROCESS_OPTIONS" of "" => () | name => let val path = Path.explode name in (case try File.read path of SOME s => set_default (decode (YXML.parse_body s)) | NONE => ()) end); val _ = load_default (); val _ = ML_Print_Depth.set_print_depth (default_int "ML_print_depth"); end; diff --git a/src/Pure/System/scala.ML b/src/Pure/System/scala.ML --- a/src/Pure/System/scala.ML +++ b/src/Pure/System/scala.ML @@ -1,105 +1,91 @@ (* Title: Pure/System/scala.ML Author: Makarius Support for Scala at runtime. *) signature SCALA = sig val functions: unit -> string list val check_function: Proof.context -> string * Position.T -> string val promise_function: string -> string -> string future val function: string -> string -> string exception Null end; structure Scala: SCALA = struct (** invoke Scala functions from ML **) val _ = Session.protocol_handler "isabelle.Scala"; (* pending promises *) val new_id = string_of_int o Counter.make (); val promises = Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table); (* invoke function *) fun promise_function name arg = let val _ = if Resources.is_pide () then () else raise Fail "PIDE session required"; val id = new_id (); fun abort () = Output.protocol_message (Markup.cancel_scala id) []; val promise = Future.promise_name "invoke_scala" abort : string future; val _ = Synchronized.change promises (Symtab.update (id, promise)); val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg]; in promise end; fun function name arg = Future.join (promise_function name arg); (* fulfill *) exception Null; fun fulfill id tag res = let val result = (case tag of "0" => Exn.Exn Null | "1" => Exn.Res res | "2" => Exn.Exn (ERROR res) | "3" => Exn.Exn (Fail res) | "4" => Exn.Exn Exn.Interrupt | _ => raise Fail "Bad tag"); val promise = Synchronized.change_result promises (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab)); val _ = Future.fulfill_result promise result; in () end; val _ = Isabelle_Process.protocol_command "Scala.fulfill" (fn [id, tag, res] => fulfill id tag res handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn); (* registered functions *) fun functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS"); -fun check_function ctxt (name, pos) = - let - val kind = Markup.scala_functionN; - val funs = functions (); - in - if member (op =) funs name then - (Context_Position.report ctxt pos (Markup.scala_function name); name) - else - let - val completion_report = - Completion.make_report (name, pos) - (fn completed => - filter completed funs - |> sort_strings - |> map (fn a => (a, (kind, a)))); - in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end - end; +fun check_function ctxt arg = + Completion.check_item Markup.scala_functionN (Markup.scala_function o #1) + (functions () |> sort_strings |> map (rpair ())) ctxt arg; val _ = Theory.setup (ML_Antiquotation.inline_embedded \<^binding>\scala_function\ (Args.context -- Scan.lift Parse.embedded_position >> (uncurry check_function #> ML_Syntax.print_string)) #> ML_Antiquotation.value_embedded \<^binding>\scala\ (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => let val name = check_function ctxt arg in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end))); end;