| /seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/ParseTree/ |
| H A D | ExportParsetreeSig.sml | 28 { file: string, startLine: FixedInt.int, startPosition: FixedInt.int,
|
| H A D | MatchCompilerSig.sml | 29 { file: string, startLine: FixedInt.int, startPosition: FixedInt.int,
|
| H A D | PrintParsetreeSig.sml | 27 { file: string, startLine: FixedInt.int, startPosition: FixedInt.int,
|
| H A D | TypeCheckParsetreeSig.sml | 29 { file: string, startLine: FixedInt.int, startPosition: FixedInt.int,
|
| /seL4-l4v-master/isabelle/src/Tools/jEdit/src/ |
| H A D | scala_console.scala | 32 File.find_files(new JFile(start), file => file.getName.endsWith(".jar")).
|
| /seL4-l4v-master/HOL4/help/src-sml/ |
| H A D | ParseDoc.sig | 26 [parse_file fname] takes fname, the name of a Doc-file, and parses it
|
| H A D | Doc2Tex.sml | 192 val file = parse_file (OS.Path.concat(dir,dnm ^ ".doc")) value
206 print_docpart(file, outstr);
207 app (fn s => print_section (s,outstr)) file;
230 " [-v] <doc directory> <TeX file>\n");
|
| H A D | ParseDoc.sml | 41 A HOL ".doc" file has the format
244 generated from the name of the file. *)
246 val ss0 = full (OS.Path.file fname)
278 val name_parts = String.tokens (equal #".") (#file (OS.Path.splitDirFile fname))
377 (* returns a set of file-names from the given directory that are .doc
|
| /seL4-l4v-master/HOL4/examples/parity/ |
| H A D | PARITYScript.sml | 2 This file needs to be processed with Holmake
|
| /seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/ |
| H A D | scala_console.scala | 32 File.find_files(new JFile(start), file => file.getName.endsWith(".jar")).
|
| /seL4-l4v-master/HOL4/tools/Holmake/ |
| H A D | HM_Core_Cline.sml | 195 desc = ReqArg (set_hmakefile, "file") },
212 { help = "don't use Overlay.sml file", long = ["no_overlay"],
218 { help = "use file as opentheory logging .uo",
219 long = ["ot"], short = "", desc = ReqArg (set_openthy, "file")},
|
| /seL4-l4v-master/HOL4/src/datatype/ |
| H A D | Datatype.sig | 30 (* into a theory file to update a datatype's basic tyinfo with extra *)
|
| /seL4-l4v-master/HOL4/src/portableML/ |
| H A D | HOLsexp.lex | 1 (* this is an -*- sml-lex -*- file *)
|
| /seL4-l4v-master/l4v/misc/ |
| H A D | isa-common.mk | 10 # This file should be included after defining a "HEAPS" variable containing the
|
| /seL4-l4v-master/HOL4/src/holyhammer/ |
| H A D | hhExportTh1.sml | 216 val file = dir ^ "/" ^ name_thm thmid ^ ".p" value
217 val oc = TextIO.openOut file
259 val file = dir ^ "/" ^ thy ^ ".ax" value
260 val oc = TextIO.openOut file
|
| H A D | hhExportSexpr.sml | 226 val file = export_dir ^ "/" ^ thy ^ ".pb" value
227 val oc = TextIO.openOut file
253 val file = sexpr_dir ^ "/theory_order.info" value
259 writel file [String.concatWith " " (sorted_ancestry thyl)]
|
| /seL4-l4v-master/isabelle/src/Pure/Admin/ |
| H A D | build_release.scala | 55 val file = dir + Path.explode(name)
56 File.write(file, f(File.read(file)))
217 Isabelle_System.bash(script, cwd = dir.file).check
338 (release.isabelle_dir + Path.explode(name)).file.delete
389 Isabelle_System.bash(script, cwd = release.dist_dir.file,
686 exe_archive.file.delete
760 other_isabelle.isabelle_home_user.file.delete
|
| H A D | build_log.scala | 81 /* file names */
96 /** log file **/
102 /* log file */
118 def apply(file: JFile): Log_File =
120 val name = file.getName
122 if (name.endsWith(".gz")) File.read_gzip(file)
123 else if (name.endsWith(".xz")) File.read_xz(file)
124 else File.read(file)
128 def apply(path: Path): Log_File = apply(path.file)
131 /* log file collection
[all...] |
| /seL4-l4v-master/isabelle/src/Tools/VSCode/src/ |
| H A D | protocol.scala | 342 sealed case class TextDocumentEdit(file: JFile, version: Long, edits: List[TextEdit])
346 "textDocument" -> JSON.Object("uri" -> Url.print_file(file), "version" -> version),
490 def apply(file: JFile, diagnostics: List[Diagnostic]): JSON.T =
492 JSON.Object("uri" -> Url.print_file(file), "diagnostics" -> diagnostics.map(_.json)))
507 def json(file: JFile): JSON.T =
509 JSON.Object("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json)))
603 def apply(file: JFile, column: Int, label: String, content: String): JSON.T =
606 "uri" -> Url.print_file(file),
|
| H A D | vscode_rendering.scala | 261 file <-
266 Line.Node_Range(file.getPath,
268 resources.get_file_content(resources.node_name(file)) match {
311 val file = perhaps_append_file(snapshot.node_name, name)
312 Some(Line.Node_Range(file) :: links)
|
| /seL4-l4v-master/l4v/isabelle/src/Tools/VSCode/src/ |
| H A D | protocol.scala | 342 sealed case class TextDocumentEdit(file: JFile, version: Long, edits: List[TextEdit])
346 "textDocument" -> JSON.Object("uri" -> Url.print_file(file), "version" -> version),
490 def apply(file: JFile, diagnostics: List[Diagnostic]): JSON.T =
492 JSON.Object("uri" -> Url.print_file(file), "diagnostics" -> diagnostics.map(_.json)))
507 def json(file: JFile): JSON.T =
509 JSON.Object("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json)))
603 def apply(file: JFile, column: Int, label: String, content: String): JSON.T =
606 "uri" -> Url.print_file(file),
|
| H A D | vscode_rendering.scala | 261 file <-
266 Line.Node_Range(file.getPath,
268 resources.get_file_content(resources.node_name(file)) match {
311 val file = perhaps_append_file(snapshot.node_name, name)
312 Some(Line.Node_Range(file) :: links)
|
| /seL4-l4v-master/l4v/isabelle/src/Pure/Admin/ |
| H A D | build_release.scala | 55 val file = dir + Path.explode(name)
56 File.write(file, f(File.read(file)))
217 Isabelle_System.bash(script, cwd = dir.file).check
338 (release.isabelle_dir + Path.explode(name)).file.delete
389 Isabelle_System.bash(script, cwd = release.dist_dir.file,
686 exe_archive.file.delete
760 other_isabelle.isabelle_home_user.file.delete
|
| H A D | build_log.scala | 81 /* file names */
96 /** log file **/
102 /* log file */
118 def apply(file: JFile): Log_File =
120 val name = file.getName
122 if (name.endsWith(".gz")) File.read_gzip(file)
123 else if (name.endsWith(".xz")) File.read_xz(file)
124 else File.read(file)
128 def apply(path: Path): Log_File = apply(path.file)
131 /* log file collection
[all...] |
| /seL4-l4v-master/HOL4/tools-poly/ |
| H A D | configure.sml | 111 replacement function: it searchs the source file for a line that
168 Generate "Systeml" file in tools-poly/Holmake and then load in that file,
278 fun to_sigobj s = bincopy s (fullPath [holdir, "sigobj", Path.file s])
284 (* if the file is this large it's been generated by Moscow ML, or is
384 val {dir=mlbdir,file=mlbfile} = OS.Path.splitDirFile mlbfile_d
386 val tgt_f = OS.Path.file tgt
388 die ("stem of mlb-file "^mlbfile_d^
389 " doesn't match file of target: "^ tgt)
392 OS.Path.joinDirFile {dir = mlbdir, file
[all...] |