val output0 = new ByteArrayOutputStream val output = new PrintStream(output0) def get_output(): String = {
output.flush()
Library.trim_line(output0.toString(UTF8.charset))
}
def context(dir: Path,
component: Boolean = false,
no_title: Boolean = false,
do_build: Boolean = false,
module: Option[Path] = None
): Context = { val props_name = if (component) isabelle.setup.Build.COMPONENT_BUILD_PROPS else isabelle.setup.Build.BUILD_PROPS val props_path = dir + Path.explode(props_name)
val props = File.read_props(props_path) if (no_title) props.remove(isabelle.setup.Build.TITLE) if (do_build) props.remove(isabelle.setup.Build.NO_BUILD) if (module.isDefined) props.put(isabelle.setup.Build.MODULE, File.standard_path(module.get))
new Context(new isabelle.setup.Build.Context(dir.java_path, props, props_path.implode))
}
object Scala_Fun extends Scala.Fun("scala_build") with Scala.Bytes_Fun { val here = Scala_Project.here def invoke(session: Session, args: List[Bytes]): List[Bytes] =
args match { case List(dir) => val result = build_result(Path.explode(dir.text)) val jar_name =
result.jar_path match { case Some(path) => path.file_name case None => "scala_build.jar"
}
List(Bytes("classpath/" + jar_name), result.jar_bytes, Bytes(result.output)) case _ => error("Bad arguments")
}
}
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.